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
---
 tactics/equality.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2d4268e60e..b037ea7e2a 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
-- 
cgit v1.2.3