From f7656793f06116377eea14b2c8f9b98db608ec5e Mon Sep 17 00:00:00 2001
From: jforest
Date: Sat, 20 May 2006 10:11:17 +0000
Subject: "subst." works now even when it exists an hypothesis have the form
 "x=x" in the goal.

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

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 1316e8aab7..6239879c99 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1140,6 +1140,8 @@ let subst_all gl =
   let test (_,c) =
     try
       let (_,x,y) = snd (find_eq_data_decompose c) in
+      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+      if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ -> 
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
     with PatternMatchingFailure -> failwith "caught"
-- 
cgit v1.2.3