diff options
| -rw-r--r-- | checker/values.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 39 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | stm/lemmas.ml | 3 | ||||
| -rw-r--r-- | stm/stm.ml | 4 |
6 files changed, 35 insertions, 18 deletions
diff --git a/checker/values.ml b/checker/values.ml index 08cb08be88..ea3df47f5c 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -109,7 +109,7 @@ let v_cstrs = let v_instance = Annot ("instance", Array v_level) let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] -let v_context_set = v_tuple "universe_context_set" [|v_set v_level;v_cstrs|] +let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index f4747c0d01..fb95ce8a6f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -41,7 +41,8 @@ let cook_this_proof p = | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = - cook_this_proof (fst (Proof_global.close_proof (fun x -> x))) + cook_this_proof (fst + (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 06ca377192..79e86e7a9f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -268,7 +268,7 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let close_proof ?feedback_id ~now fpl = +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 @@ -280,22 +280,34 @@ let close_proof ?feedback_id ~now fpl = (* Because of dependent subgoals at the begining 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 = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in + let subst_evar k = + Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar (Evd.evar_universe_context_subst universes) in let make_body = if poly || now then let make_body t (c, eff) = + let open Universes in let body = c and typ = nf t in - let used_univs = - Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) - 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 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 + if keep_body_ucst_sepatate then + (* For vi2vo compilation proofs are computed now but we need to + * completent the univ constraints of the typ with the ones of + * the body. So we keep the two sets distinct. *) + let ctx_body = restrict_universe_context ctx used_univs_body in + let ctx_typ = restrict_universe_context ctx used_univs_typ in + let univs_typ = Univ.ContextSet.to_context ctx_typ in + (univs_typ, typ), ((body, ctx_body), eff) + else + (* 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 *) + let used_univs = Univ.LSet.union used_univs_body used_univs_typ in + let ctx = restrict_universe_context ctx used_univs in + 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)) @@ -350,9 +362,10 @@ let return_proof () = proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = - close_proof ~feedback_id ~now:false proof -let close_proof fix_exn = - close_proof ~now:true (Future.from_val ~fix_exn (return_proof ())) + close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof +let close_proof ~keep_body_ucst_sepatate fix_exn = + close_proof ~keep_body_ucst_sepatate ~now:true + (Future.from_val ~fix_exn (return_proof ())) (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 1a13edf17e..c2c447c92c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -91,7 +91,7 @@ val start_dependent_proof : (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : Future.fix_exn -> closed_proof +val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The formes is supposed to be diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 4bc6f4ee63..48ec66ce63 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -462,7 +462,8 @@ let save_proof ?proof = function | Vernacexpr.Proved (is_opaque,idopt) -> let (proof_obj,terminator) = match proof with - | None -> Proof_global.close_proof (fun x -> x) + | None -> + Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x) | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) diff --git a/stm/stm.ml b/stm/stm.ml index 72f7dcbe7a..c966d9bb86 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1126,7 +1126,8 @@ end = struct (* {{{ *) Proof_global.set_terminator (Lemmas.standard_proof_terminator [] (Lemmas.mk_hook (fun _ _ -> ()))); - let proof = Proof_global.close_proof (fun x -> x) in + let proof = + Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in vernac_interp stop ~proof { verbose = false; loc; expr = (VernacEndProof (Proved (true,None))) }; @@ -1705,6 +1706,7 @@ let known_state ?(redefine_qed=false) ~cache id = let proof = if keep != VtKeep then None else Some(Proof_global.close_proof + ~keep_body_ucst_sepatate:false (State.exn_on id ~valid:eop)) in if proof = None then prerr_endline "NONE!!!!!"; reach view.next; |