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

4 files changed, 9 insertions, 14 deletions

diff --git a/CHANGES b/CHANGES
index 6b071342b..1cf857df9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,6 +55,8 @@ Tactics
   automatically the dependencies over the arguments of the types
   (based on initial ideas from Chung-Kil Hur, extension to nested
    dependencies suggested by Dan Grayson)
+- Tactic "injection" now failing on an equality showing no constructors while
+  it was formerly generalizing again the goal over the given equality.
 
 Vernacular commands
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4917c64f4..0b04a572f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -513,15 +513,6 @@ and intros_with_rewrite_aux : tactic =
 				     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;
-				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Equality.rewriteRL (mkVar id));
-				     intros_with_rewrite
-				   ]
-			  g
 		      else
 			begin
 			  let id = pf_get_new_id (id_of_string "y") g  in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2d4268e60..b037ea7e2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -568,7 +568,7 @@ let discriminable env sigma t1 t2 =
 
 let injectable env sigma t1 t2 =
     match find_positions env sigma t1 t2 with
-    | Inl _ | Inr [] -> false
+    | Inl _ | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
 
 
@@ -1112,6 +1112,8 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
     | Inr [] ->
 	errorlabstrm "Equality.inj"
 	   (str"Nothing to do, it is an equality between convertible terms.")
+    | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
+        errorlabstrm "Equality.inj" (str"Nothing to inject.")
     | Inr posns ->
 (* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
 	let t1 = try_delta_expand env sigma t1 in
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 24bc291de..958ecd4ff 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -250,12 +250,12 @@ case H0; simpl in |- *; auto.
 case m; simpl in |- *; auto.
 case (index 0 s1 s2'); intros; discriminate.
 intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
-intros x H H0 H1; apply H; injection H1; intros H2; injection H2; auto.
+intros x H H0 H1; apply H; injection H1; auto.
 intros; discriminate.
 intros n'; case m; simpl in |- *; auto.
 case (index n' s1 s2'); intros; discriminate.
 intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
-intros x H H1; apply H; injection H1; intros H2; injection H2; auto.
+intros x H H1; apply H; injection H1; auto.
 intros; discriminate.
 Qed.
 
@@ -288,7 +288,7 @@ intros x H H0 H1 p; try case p; simpl in |- *; auto.
 intros H2 H3; red in |- *; intros H4; case H0.
 intros H5 H6; absurd (false = true); auto with bool.
 intros n0 H2 H3; apply H; auto.
-injection H1; intros H4; injection H4; auto.
+injection H1; auto.
 apply Le.le_O_n.
 apply Lt.lt_S_n; auto.
 intros; discriminate.
@@ -298,7 +298,7 @@ intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
 intros x H H0 p; case p; simpl in |- *; auto.
 intros H1; inversion H1; auto.
 intros n0 H1 H2; apply H; auto.
-injection H0; intros H3; injection H3; auto.
+injection H0; auto.
 apply Le.le_S_n; auto.
 apply Lt.lt_S_n; auto.
 intros; discriminate.