diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:04:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:11:38 +0100 |
| commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
| tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /proofs/proof_global.mli | |
| parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
| parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 929bb86e8..a67481e71 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -58,7 +58,7 @@ type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -100,7 +100,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) |