sig
val mk_mset :
EConstr.constr -> (EConstr.constr * int) list -> EConstr.constr
module Sigma :
sig
val add :
EConstr.constr ->
EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
val empty : EConstr.constr -> EConstr.constr
val of_list :
EConstr.constr ->
EConstr.constr -> (int * EConstr.constr) list -> EConstr.constr
val to_fun :
EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr
end
module Sym :
sig
type pack = { ar : Constr.t; value : Constr.t; morph : Constr.t; }
val typ : Coq.lazy_ref
val mk_pack : Coq.Relation.t -> Theory.Sym.pack -> EConstr.constr
val null : Coq.Relation.t -> EConstr.constr
end
module Stubs :
sig
val lift : Coq.lazy_ref
val lift_proj_equivalence : Coq.lazy_ref
val lift_transitivity_left : Coq.lazy_ref
val lift_transitivity_right : Coq.lazy_ref
val lift_reflexivity : Coq.lazy_ref
val eval : Coq.lazy_ref
val decide_thm : Coq.lazy_ref
val lift_normalise_thm : Coq.lazy_ref
end
module Trans :
sig
type envs
val empty_envs : unit -> Theory.Trans.envs
val t_of_constr :
Environ.env ->
Evd.evar_map ->
Coq.Relation.t ->
Theory.Trans.envs ->
EConstr.constr * EConstr.constr ->
Matcher.Terms.t * Matcher.Terms.t * Evd.evar_map
val add_symbol :
Environ.env ->
Evd.evar_map ->
Coq.Relation.t -> Theory.Trans.envs -> Constr.t -> Evd.evar_map
type ir
val ir_of_envs :
Environ.env ->
Evd.evar_map ->
Coq.Relation.t -> Theory.Trans.envs -> Evd.evar_map * Theory.Trans.ir
val ir_to_units : Theory.Trans.ir -> Matcher.ext_units
val raw_constr_of_t :
Theory.Trans.ir ->
Coq.Relation.t ->
EConstr.rel_context -> Matcher.Terms.t -> EConstr.constr
type sigmas = {
env_sym : EConstr.constr;
env_bin : EConstr.constr;
env_units : EConstr.constr;
}
type reifier
val mk_reifier :
Coq.Relation.t ->
EConstr.constr ->
Theory.Trans.ir ->
(Theory.Trans.sigmas * Theory.Trans.reifier) Proofview.tactic
val reif_constr_of_t :
Theory.Trans.reifier -> Matcher.Terms.t -> EConstr.constr
end
end