From a0e792236c9666df1069753f8f807c12f713dcfb Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 23 Mar 2016 16:03:47 +0100
Subject: refine: do check all unif problems are solved (Close: #4415, #4532)

This fixes a class of bugs like

  refine foo; tactic.

where tactic fails (by resuming the remaining, unsolvable, problems) while
in 8.4 refine was failing.

It is not clear to us (Maxime and myself) if we should call
consider_remaining_unif_problems instead of check_problems_are_solved.
---
 proofs/proofview.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6d7dcb9257..80569e2342 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1061,6 +1061,7 @@ struct
   let typecheck_proof c concl env sigma =
     let evdref = ref sigma in
     let () = Typing.check env evdref c concl in
+    Evarconv.check_problems_are_solved env !evdref;
     !evdref
 
   let (pr_constrv,pr_constr) =
-- 
cgit v1.2.3


From 31ffc14b4b8d531777042d3ff02f34985bcec084 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 23 Mar 2016 18:26:00 +0100
Subject: Revert "refine: do check all unif problems are solved (Close: #4415,
 #4532)"

This fix is too restrictive.  Still, opening a goal for an evar with a
pending conv_pb is unsafe since the user may prove (instantiate it) in
a way not compatible with the conv_pb.

Assigning an evar, in its lowest level API, should enforce that all
related conv_pbs are satisfied by the instance.
This also poses a UI problem, since there is not way to see these
conv_pbs.  One could print a goal and say: look, the proof term you give
must validate this equation...

Given that the good fix is not obvious, we revert!

This reverts commit a0e792236c9666df1069753f8f807c12f713dcfb.
---
 proofs/proofview.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 80569e2342..6d7dcb9257 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1061,7 +1061,6 @@ struct
   let typecheck_proof c concl env sigma =
     let evdref = ref sigma in
     let () = Typing.check env evdref c concl in
-    Evarconv.check_problems_are_solved env !evdref;
     !evdref
 
   let (pr_constrv,pr_constr) =
-- 
cgit v1.2.3


From 7e7b5684d8f8066b90fca3395104af7241b8aed6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 25 Mar 2016 16:46:50 +0100
Subject: Univs: fix get_current_context (bug #4603, part I)

Return an evar_map with the right universes, when there are no focused
subgoals or the proof is finished.
---
 proofs/pfedit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index b635cc9632..2f5c1d1c2b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -85,7 +85,8 @@ let get_current_goal_context () =
   with NoSuchGoal ->
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
-    (Evd.empty, Global.env ())
+    let env = Global.env () in
+    (Evd.from_env env, env)
 
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
-- 
cgit v1.2.3