diff options
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index f10e991ea..6c11ee9b4 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -61,6 +61,8 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; + constraints : Univ.constraints; + (** guards : lemma_possible_guards; *) } type proof_ending = |