sig
val init_constant : string list -> string -> Term.constr
type goal_sigma = Proof_type.goal Tacmach.sigma
val goal_update : AAC_coq.goal_sigma -> Evd.evar_map -> AAC_coq.goal_sigma
val resolve_one_typeclass :
Proof_type.goal Tacmach.sigma ->
Term.types -> Term.constr * AAC_coq.goal_sigma
val cps_resolve_one_typeclass :
?error:string ->
Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val nf_evar : AAC_coq.goal_sigma -> Term.constr -> Term.constr
val fresh_evar :
AAC_coq.goal_sigma -> Term.types -> Term.constr * AAC_coq.goal_sigma
val evar_unit :
AAC_coq.goal_sigma -> Term.constr -> Term.constr * AAC_coq.goal_sigma
val evar_binary :
AAC_coq.goal_sigma -> Term.constr -> Term.constr * AAC_coq.goal_sigma
val evar_relation :
AAC_coq.goal_sigma -> Term.constr -> Term.constr * AAC_coq.goal_sigma
val cps_evar_relation :
Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val cps_mk_letin :
string ->
Term.constr -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val decomp_term :
Term.constr -> (Term.constr, Term.types) Term.kind_of_term
val lapp : Term.constr lazy_t -> Term.constr array -> Term.constr
module List :
sig
val of_list : Term.constr -> Term.constr list -> Term.constr
val type_of_list : Term.constr -> Term.constr
end
module Pair :
sig
val typ : Term.constr lazy_t
val pair : Term.constr lazy_t
val of_pair :
Term.constr ->
Term.constr -> Term.constr * Term.constr -> Term.constr
end
module Bool :
sig val typ : Term.constr lazy_t val of_bool : bool -> Term.constr end
module Comparison :
sig
val typ : Term.constr lazy_t
val eq : Term.constr lazy_t
val lt : Term.constr lazy_t
val gt : Term.constr lazy_t
end
module Leibniz :
sig val eq_refl : Term.types -> Term.constr -> Term.constr end
module Option :
sig
val some : Term.constr -> Term.constr -> Term.constr
val none : Term.constr -> Term.constr
val of_option : Term.constr -> Term.constr option -> Term.constr
end
module Pos :
sig val typ : Term.constr lazy_t val of_int : int -> Term.constr end
module Nat :
sig val typ : Term.constr lazy_t val of_int : int -> Term.constr end
module Classes :
sig
val mk_morphism :
Term.constr -> Term.constr -> Term.constr -> Term.constr
val mk_equivalence : Term.constr -> Term.constr -> Term.constr
val mk_reflexive : Term.constr -> Term.constr -> Term.constr
val mk_transitive : Term.constr -> Term.constr -> Term.constr
end
module Relation :
sig
type t = { carrier : Term.constr; r : Term.constr; }
val make : Term.constr -> Term.constr -> AAC_coq.Relation.t
val split : AAC_coq.Relation.t -> Term.constr * Term.constr
end
module Transitive :
sig
type t = {
carrier : Term.constr;
leq : Term.constr;
transitive : Term.constr;
}
val make :
Term.constr -> Term.constr -> Term.constr -> AAC_coq.Transitive.t
val infer :
AAC_coq.goal_sigma ->
Term.constr ->
Term.constr -> AAC_coq.Transitive.t * AAC_coq.goal_sigma
val from_relation :
AAC_coq.goal_sigma ->
AAC_coq.Relation.t -> AAC_coq.Transitive.t * AAC_coq.goal_sigma
val cps_from_relation :
AAC_coq.Relation.t ->
(AAC_coq.Transitive.t -> Proof_type.tactic) -> Proof_type.tactic
val to_relation : AAC_coq.Transitive.t -> AAC_coq.Relation.t
end
module Equivalence :
sig
type t = {
carrier : Term.constr;
eq : Term.constr;
equivalence : Term.constr;
}
val make :
Term.constr -> Term.constr -> Term.constr -> AAC_coq.Equivalence.t
val infer :
AAC_coq.goal_sigma ->
Term.constr ->
Term.constr -> AAC_coq.Equivalence.t * AAC_coq.goal_sigma
val from_relation :
AAC_coq.goal_sigma ->
AAC_coq.Relation.t -> AAC_coq.Equivalence.t * AAC_coq.goal_sigma
val cps_from_relation :
AAC_coq.Relation.t ->
(AAC_coq.Equivalence.t -> Proof_type.tactic) -> Proof_type.tactic
val to_relation : AAC_coq.Equivalence.t -> AAC_coq.Relation.t
val split :
AAC_coq.Equivalence.t -> Term.constr * Term.constr * Term.constr
end
val match_as_equation :
?context:Term.rel_context ->
AAC_coq.goal_sigma ->
Term.constr -> (Term.constr * Term.constr * AAC_coq.Relation.t) option
val tclTIME : string -> Proof_type.tactic -> Proof_type.tactic
val tclDEBUG : string -> Proof_type.tactic -> Proof_type.tactic
val tclPRINT : Proof_type.tactic -> Proof_type.tactic
val anomaly : string -> 'a
val user_error : string -> 'a
val warning : string -> unit
module Rewrite :
sig
type hypinfo = {
hyp : Term.constr;
hyptype : Term.constr;
context : Term.rel_context;
body : Term.constr;
rel : AAC_coq.Relation.t;
left : Term.constr;
right : Term.constr;
l2r : bool;
}
val get_hypinfo :
Term.constr ->
l2r:bool ->
?check_type:(Term.types -> bool) ->
(AAC_coq.Rewrite.hypinfo -> Proof_type.tactic) -> Proof_type.tactic
val build :
AAC_coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val build_with_evar :
AAC_coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val rewrite :
?abort:bool ->
AAC_coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
end
end