sig
val init_constant : string list -> string -> Term.constr
type goal_sigma = Proof_type.goal Tacmach.sigma
val goal_update : Coq.goal_sigma -> Evd.evar_map -> Coq.goal_sigma
val resolve_one_typeclass :
Proof_type.goal Tacmach.sigma ->
Term.types -> Term.constr * Coq.goal_sigma
val cps_resolve_one_typeclass :
?error:string ->
Term.types -> (Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val nf_evar : Coq.goal_sigma -> Term.constr -> Term.constr
val fresh_evar :
Coq.goal_sigma -> Term.types -> Term.constr * Coq.goal_sigma
val evar_unit :
Coq.goal_sigma -> Term.constr -> Term.constr * Coq.goal_sigma
val evar_binary :
Coq.goal_sigma -> Term.constr -> Term.constr * Coq.goal_sigma
val evar_relation :
Coq.goal_sigma -> Term.constr -> Term.constr * 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
val eq : Term.types -> 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 -> Coq.Relation.t
val split : 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 -> Coq.Transitive.t
val infer :
Coq.goal_sigma ->
Term.constr -> Term.constr -> Coq.Transitive.t * Coq.goal_sigma
val from_relation :
Coq.goal_sigma -> Coq.Relation.t -> Coq.Transitive.t * Coq.goal_sigma
val cps_from_relation :
Coq.Relation.t ->
(Coq.Transitive.t -> Proof_type.tactic) -> Proof_type.tactic
val to_relation : Coq.Transitive.t -> 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 -> Coq.Equivalence.t
val infer :
Coq.goal_sigma ->
Term.constr -> Term.constr -> Coq.Equivalence.t * Coq.goal_sigma
val from_relation :
Coq.goal_sigma ->
Coq.Relation.t -> Coq.Equivalence.t * Coq.goal_sigma
val cps_from_relation :
Coq.Relation.t ->
(Coq.Equivalence.t -> Proof_type.tactic) -> Proof_type.tactic
val to_relation : Coq.Equivalence.t -> Coq.Relation.t
val split :
Coq.Equivalence.t -> Term.constr * Term.constr * Term.constr
end
val match_as_equation :
?context:Term.rel_context ->
Coq.goal_sigma ->
Term.constr -> (Term.constr * Term.constr * 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 : Coq.Relation.t;
left : Term.constr;
right : Term.constr;
l2r : bool;
}
val get_hypinfo :
Term.constr ->
l2r:bool ->
?check_type:(Term.types -> bool) ->
(Coq.Rewrite.hypinfo -> Proof_type.tactic) -> Proof_type.tactic
val build :
Coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val build_with_evar :
Coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Term.constr -> Proof_type.tactic) -> Proof_type.tactic
val rewrite :
?abort:bool ->
Coq.Rewrite.hypinfo ->
(int * Term.constr) list ->
(Proof_type.tactic -> Proof_type.tactic) -> Proof_type.tactic
end
end