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