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;
sigma : Evd.evar_map;
}