diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 33 |
1 files changed, 15 insertions, 18 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5bff3c813..3e2c813e3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -273,12 +273,10 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in + let initial_euctx = Proof.initial_euctx proof in let fpl, univs = Future.split2 fpl in - let universes = - if poly || now then Future.force univs - else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) - in - (* Because of dependent subgoals at the begining of proofs, we could + let universes = if poly || now then Future.force univs else initial_euctx in + (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = @@ -289,11 +287,12 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = if poly || now then let make_body t (c, eff) = let open Universes in - let body = c and typ = nf t in + let body = c and typ = nf t in let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in - let ctx = Evd.evar_universe_context_set universes in + let used_univs_typ = Universes.universes_of_constr typ in if keep_body_ucst_sepatate then + let initunivs = Evd.evar_context_universe_context initial_euctx in + let ctx = Evd.evar_universe_context_set initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -302,6 +301,8 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let univs_typ = Univ.ContextSet.to_context ctx_typ in (univs_typ, typ), ((body, ctx_body), eff) else + let initunivs = Univ.UContext.empty in + let ctx = Evd.evar_universe_context_set initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -310,14 +311,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl = let univs = Univ.ContextSet.to_context ctx in (univs, typ), ((body, Univ.ContextSet.empty), eff) in - fun t p -> - Future.split2 (Future.chain ~pure:true p (make_body t)) + fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t)) else fun t p -> - let initunivs = Evd.evar_context_universe_context universes in - Future.from_val (initunivs, nf t), - Future.chain ~pure:true p (fun (pt,eff) -> - (pt, Evd.evar_universe_context_set (Future.force univs)), eff) + let initunivs = Evd.evar_context_universe_context initial_euctx in + Future.from_val (initunivs, nf t), + Future.chain ~pure:true p (fun (pt,eff) -> + (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -370,10 +370,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = - if poly || !Flags.compilation_mode = Flags.BuildVo - then Evd.nf_constraints evd - else evd in + let evd = Evd.nf_constraints evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) |