From 56d4015ec3e49d2cfba90d6617e041a365bdeec9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Oct 2011 12:34:08 +0000
Subject: Fixing Equality.injectable which did not detect an equality without
 constructors as non relevant for injection. Also made injection failing in
 such situation.

Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases
(observed in the compilation of CoinductiveReals.LNP_Digit). The
most probable explanation is that this loop was formerly protected by
a failing rewrite which stopped failing after revision 14549 made
second-order pattern-matching more powerful.

Also suppressed dead code in Invfun.intros_with_rewrite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/invfun.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4917c64f41..0b04a572fe 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -505,15 +505,6 @@ and intros_with_rewrite_aux : tactic =
 				   ]
 			  g
 		      else if isVar args.(2) 
-		      then 
-			let id = pf_get_new_id (id_of_string "y") g  in
-			tclTHENSEQ [ h_intro id;
-				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Equality.rewriteRL (mkVar id));
-				     intros_with_rewrite
-				   ]
-			  g
-		      else if isVar args.(2) 
 		      then 
 			let id = pf_get_new_id (id_of_string "y") g  in
 			tclTHENSEQ [ h_intro id;
-- 
cgit v1.2.3