From 4cb7fe525a472928aee02d772458d28a2b71072a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 19:21:05 +0200
Subject: - Fix arity handling in retyping (de Bruijn bug!) - Enforce that no u
 <= Prop/Set can be added for u introduced by the user in
 Evd.process_constraints. (Needs to be enforced in the kernel as well, but
 that's the main entry point). - Fix a test-suite script and remove a
 regression comment, it's just as before now.

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

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c6c4049923..dc9cc471c2 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -633,12 +633,12 @@ let unify_eqn env (sigma, cstrs) hypinfo by t =
 	  and ty2 = Typing.type_of env'.env env'.evd c2
 	  in
 	    if convertible env env'.evd ty1 ty2 then 
-	      (if occur_meta_or_existential prf then
+	      (* (if occur_meta_or_existential prf then *)
 		(hypinfo := refresh_hypinfo env env'.evd !hypinfo;
 		 env'.evd, prf, c1, c2, car, rel)
-	       else (** Evars have been solved, we can go back to the initial evd,
-			but keep the potential refinement of existing evars. *)
-		  env'.evd, prf, c1, c2, car, rel)
+	       (* else (\** Evars have been solved, we can go back to the initial evd, *)
+	       (* 		but keep the potential refinement of existing evars. *\) *)
+	       (* 	  env'.evd, prf, c1, c2, car, rel) *)
 	    else raise Reduction.NotConvertible
     in
     let evars = evd', Evar.Set.empty in
-- 
cgit v1.2.3