sig
type envs
val empty_envs : unit -> Theory.Trans.envs
val t_of_constr :
Coq.goal_sigma ->
Coq.Relation.t ->
Theory.Trans.envs ->
EConstr.constr * EConstr.constr ->
Matcher.Terms.t * Matcher.Terms.t * Coq.goal_sigma
val add_symbol :
Coq.goal_sigma ->
Coq.Relation.t -> Theory.Trans.envs -> Constr.t -> Coq.goal_sigma
type ir
val ir_of_envs :
Coq.goal_sigma ->
Coq.Relation.t -> Theory.Trans.envs -> Coq.goal_sigma * 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 -> Proof_type.tactic) ->
Proof_type.tactic
val reif_constr_of_t :
Theory.Trans.reifier -> Matcher.Terms.t -> EConstr.constr
end