Merge branch 'v8.5'

4 files changed, 26 insertions, 23 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 18883df24..aaa49f116 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -125,7 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when Errors.noncritical e ->
-      (** This is Tacticals.tclFAIL *)
-      Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
+    with e when Errors.noncritical e -> Proofview.tclZERO e
   end
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 828f9fa71..a7077d911 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -111,6 +111,8 @@ type proof = {
   shelf : Goal.goal list;
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
+  (* The initial universe context (for the statement) *)
+  initial_euctx : Evd.evar_universe_context
 }
 
 (*** General proof functions ***)
@@ -271,7 +273,9 @@ let start sigma goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 let dependent_start goals =
   let entry, proofview = Proofview.dependent_init goals in
@@ -280,7 +284,9 @@ let dependent_start goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -311,6 +317,7 @@ let return p =
     Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.entry
+let initial_euctx p = p.initial_euctx
 
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2b85ec872..a2e10d813 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -69,6 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
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... *)