diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 80 |
1 files changed, 28 insertions, 52 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7c44f1500d..410335b47e 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -63,7 +63,7 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = Universes.universe_opt_subst Univ.in_universe_context +type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; @@ -222,22 +222,22 @@ let disactivate_proof_mode mode = is (spiwack: for potential printing, I believe is used only by closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. *) -let start_proof id str goals terminator = +let start_proof id str ctx goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.start (Evd.from_env (Global.env ())) goals; + proof = Proof.start (Evd.from_env ~ctx (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; mode = find_proof_mode "No" } in push initial_state pstates -let start_dependent_proof id str goals terminator = +let start_dependent_proof id str ctx goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals; + proof = Proof.dependent_start (Evd.from_env ~ctx (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; @@ -269,54 +269,33 @@ let close_proof ?feedback_id ~now fpl = let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in - let univsubst, make_body = + let universes = Future.force univs in + let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) + (Evd.evar_universe_context_subst universes) in + let make_body = if poly || now then - let make_usubst (usubst, uctx) = - let ctx, subst = - Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) - in - let nf x = - let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in - Vars.subst_univs_level_constr subst (nf x) - in - let subst = - Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst) - in - let univsubst = (subst, Univ.ContextSet.to_context ctx) in - univsubst, nf - in - let make_body nf ctx t _octx ((c, _ctx), eff) = - let body = nf c and typ = nf t in + let make_body t ((c, _ctx), eff) = + let body = c and typ = nf t in let used_univs = Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) + (Universes.universes_of_constr typ) in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) used_univs in - let p = (body, Univ.ContextSet.empty),eff in + let ctx = Evd.evar_universe_context_set universes in + let ctx = Universes.restrict_universe_context ctx used_univs in let univs = Univ.ContextSet.to_context ctx in + let p = (body, Univ.ContextSet.empty), eff in (univs, typ), p - in - let make_body nf ctx t octx p = - Future.split2 (Future.chain ~pure:true p (make_body nf ctx t octx)) - in - let univsubst = - Future.chain ~pure:true univs make_usubst - in univsubst, make_body + in + fun t p -> + Future.split2 (Future.chain ~pure:true p (make_body t)) else - let ctx = - List.fold_left (fun acc (c, (t, octx)) -> - Univ.ContextSet.union octx acc) - Univ.ContextSet.empty initial_goals - in - let univs = Univ.ContextSet.to_context ctx in - let univsubst = (Univ.LMap.empty, univs) in - let make_body nf ctx t octx p = Future.from_val (univs, t), p in - Future.from_val (univsubst, fun x -> x), make_body + let univs = Evd.evar_context_universe_context universes in + fun t p -> + Future.from_val (univs, nf t), p in - let univsubst, nf = Future.force univsubst in let entries = - Future.map2 (fun p (c, (t, octx)) -> - let univstyp, body = make_body nf (snd univsubst) t octx p in + Future.map2 (fun p (c, t) -> + let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in { Entries. const_entry_body = body; @@ -329,11 +308,10 @@ let close_proof ?feedback_id ~now fpl = const_entry_polymorphic = poly; const_entry_proj = false}) fpl initial_goals in - { id = pid; entries = entries; persistence = strength; universes = univsubst }, + { id = pid; entries = entries; persistence = strength; universes = universes }, Ephemeron.get terminator -type closed_proof_output = Entries.proof_output list * - Universes.universe_opt_subst Univ.in_universe_context +type closed_proof_output = Entries.proof_output list * Evd.evar_universe_context let return_proof () = let { proof } = cur_pstate () in @@ -352,14 +330,12 @@ let return_proof () = str"variables still non-instantiated") in let eff = Evd.eval_side_effects evd in let evd = Evd.nf_constraints evd in - let subst = Evd.universe_subst evd in - let ctx = Evd.universe_context_set 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... *) let proofs = - List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, ctx), eff)) initial_goals in - proofs, (subst, Univ.ContextSet.to_context ctx) + List.map (fun (c, _) -> ((Evarutil.nf_evars_universes evd c, Univ.ContextSet.empty), eff)) initial_goals in + proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = close_proof ~feedback_id ~now:false proof @@ -523,7 +499,7 @@ module V82 = struct let get_current_initial_conclusions () = let { pid; strength; proof } = cur_pstate () in let initial = Proof.initial_goals proof in - let goals = List.map (fun (o, (c, ctx)) -> c) initial in + let goals = List.map (fun (o, c) -> c) initial in pid, (goals, strength) end |