Vi2vo: fix handling of univ constraints coming from the body

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;