diff options
| author | jforest | 2006-05-20 10:11:17 +0000 |
|---|---|---|
| committer | jforest | 2006-05-20 10:11:17 +0000 |
| commit | f7656793f06116377eea14b2c8f9b98db608ec5e (patch) | |
| tree | d332e0f1ffa7ce469cbe1a4b934d9b5a8e15b865 | |
| parent | 99dfd9ba50a40df6c3d558b84ce2a8284ab16fa0 (diff) | |
"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
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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" |