Module Lemmas.Proof_ending

Creating high-level proofs with an associated constant

type t =
| Regular
| End_obligation of DeclareObl.obligation_qed_info
| End_derive of {
f : Names.Id.t;
name : Names.Id.t;
}
| End_equations of {
hook : Names.Constant.t list -> Evd.evar_map -> unit;
i : Names.Id.t;
types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list;
wits : EConstr.t list Stdlib.ref;
sigma : Evd.evar_map;
}