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(+)

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