diff options
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 |