From 9a24bc736d5782b7b9c23ebd4cfcf5f5f99836eb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 20 Aug 2014 01:42:40 +0200
Subject: Removing a Goal.sensitive in Rewrite.

---
 tactics/rewrite.ml | 38 ++++++++++++++++++--------------------
 1 file changed, 18 insertions(+), 20 deletions(-)

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a9c60a1edf..5d4a7509aa 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1456,9 +1456,6 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
   in tac gl
 
 
-let bind_gl_info f =
-  bind concl (fun c -> bind env (fun v -> bind defs (fun ev -> f c v ev))) 
-
 let new_refine (evd, c) =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
@@ -1524,23 +1521,24 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	| None, (undef, None, newt) ->
             Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast)
   in
-  let info =
-    bind_gl_info
-      (fun concl env sigma ->
-	 let ty, is_hyp =
-	   match clause with
-	   | Some id -> Environ.named_type id env, Some id
-	   | None -> concl, None
-	 in
-	   try 
-	     let res = 
-	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
-	     in return (res, is_hyp)
-	   with
-	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
-			++ fnl () ++ Himsg.explain_typeclass_error env e)))
-  in Proofview.Goal.lift info (fun i -> treat i)
+  Proofview.Goal.enter begin fun gl ->
+    let concl = Proofview.Goal.concl gl in
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let ty, is_hyp =
+      match clause with
+      | Some id -> Environ.named_type id env, Some id
+      | None -> concl, None
+    in
+    try
+      let res =
+        cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
+      in treat (res, is_hyp)
+    with
+    | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
+      raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
+                ++ fnl () ++ Himsg.explain_typeclass_error env e))
+  end
 
 let newtactic_init_setoid () =
   try init_setoid (); Proofview.tclUNIT ()
-- 
cgit v1.2.3