From 7c4d29628a58d0192b76aebf8da29644019aee1c Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 20 Feb 2012 20:54:12 +0000
Subject: Use a heuristic to not simplify equality hypotheses remaining after
 dependent induction if they don't look really trivial. We still are making a
 choice though. Fixes bug #2712.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 96ddc730e7..11b0b9b81c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2503,11 +2503,17 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
 				   tclMAP (fun id -> 
 				     tclTRY (generalize_dep ~with_let:true (mkVar id))) vars] gl) gl
 
+let rec compare_upto_variables x y =
+  if (isVar x || isRel x) && (isVar y || isRel y) then true
+  else compare_constr compare_upto_variables x y
+
 let specialize_eqs id gl =
   let env = pf_env gl in
   let ty = pf_get_hyp_typ gl id in
   let evars = ref (project gl) in
-  let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
+  let unif env evars c1 c2 = 
+    compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2 
+  in
   let rec aux in_eqs ctx acc ty =
     match kind_of_term ty with
     | Prod (na, t, b) -> 
-- 
cgit v1.2.3