sig
type tactic = unit Proofview.tactic
type lazy_ref = Names.GlobRef.t Stdlib.Lazy.t
val get_fresh : Coq.lazy_ref -> Constr.constr
val get_efresh : Coq.lazy_ref -> EConstr.constr
val find_global : string -> Coq.lazy_ref
val cps_resolve_one_typeclass :
?error:Pp.t ->
EConstr.types -> (EConstr.constr -> Coq.tactic) -> Coq.tactic
val evar_binary :
Environ.env ->
Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
val evar_relation :
Environ.env ->
Evd.evar_map -> EConstr.constr -> Evd.evar_map * EConstr.constr
val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic
val tclRETYPE : EConstr.constr -> unit Proofview.tactic
val decomp_term :
Evd.evar_map ->
EConstr.constr ->
(EConstr.constr, EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t,
EConstr.ERelevance.t)
Constr.kind_of_term
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 : Coq.lazy_ref
val pair : Coq.lazy_ref
val of_pair :
EConstr.constr ->
EConstr.constr -> EConstr.constr * EConstr.constr -> EConstr.constr
end
module Option :
sig
val typ : Coq.lazy_ref
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 : Coq.lazy_ref val of_int : int -> EConstr.constr end
module Nat :
sig val typ : Coq.lazy_ref val of_int : int -> Constr.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 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 :
Environ.env ->
Evd.evar_map ->
EConstr.constr -> EConstr.constr -> Coq.Equivalence.t * Evd.evar_map
val from_relation :
Environ.env ->
Evd.evar_map -> Coq.Relation.t -> Coq.Equivalence.t * Evd.evar_map
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 ->
Environ.env ->
Evd.evar_map ->
EConstr.constr ->
(EConstr.constr * EConstr.constr * Coq.Relation.t) option
val tclTIME : string -> Coq.tactic -> Coq.tactic
val tclDEBUG : string -> unit Proofview.tactic
val tclPRINT : unit Proofview.tactic
val anomaly : string -> 'a
val user_error : Pp.t -> 'a
val warning : string -> unit
val show_proof : Declare.Proof.t -> 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 :
Environ.env ->
Evd.evar_map ->
?check_type:(EConstr.types -> bool) ->
EConstr.constr -> l2r:bool -> Coq.Rewrite.hypinfo
val build :
Coq.Rewrite.hypinfo -> (int * EConstr.constr) list -> EConstr.constr
val rewrite :
?abort:bool ->
Coq.Rewrite.hypinfo ->
(int * EConstr.constr) list -> unit Proofview.tactic
end
end