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.ml | |
parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'proofs/proof_global.ml')
-rw-r--r-- | proofs/proof_global.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4af18ab2d..e036ae3a1 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -67,7 +67,7 @@ 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; *) @@ -323,13 +323,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let open Universes in let body = c in let typ = - if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then + if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then + if keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to @@ -373,7 +374,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, fun pr_ending -> Ephemeron.get terminator pr_ending -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 let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in |