From 8fcdb5bcddb7c238bb15895156821ea8c12da993 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 Feb 2015 09:35:59 +0100
Subject: Fixing bug #3944.

---
 tactics/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 9289c6d663..c898ca401d 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -283,7 +283,7 @@ end) = struct
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 	(* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
       else if bp then (* Dummy forall *)
-	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
+	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall
       else (* None in Prop, use arrow *)
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 
-- 
cgit v1.2.3


From 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 18 Feb 2015 17:08:28 +0100
Subject: Fix bug #3938

---
 tactics/rewrite.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c898ca401d..ac8b4923e5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1444,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       let newt = Evarutil.nf_evar evars' res.rew_to in
       let evars = (* Keep only original evars (potentially instantiated) and goal evars,
 		     the rest has been defined and substituted already. *)
-	Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars'
+	Evar.Set.fold 
+	  (fun ev acc -> 
+	   if not (Evd.is_defined acc ev) then 
+	     errorlabstrm "rewrite"
+			  (str "Unsolved constraint remaining: " ++ spc () ++
+			   Evd.pr_evar_info (Evd.find acc ev))
+	   else Evd.remove acc ev) 
+	  cstrs evars'
       in
       let res = match res.rew_prf with
 	| RewCast c -> None
-- 
cgit v1.2.3