diff options
| author | puech | 2011-07-29 14:25:40 +0000 |
|---|---|---|
| committer | puech | 2011-07-29 14:25:40 +0000 |
| commit | ad910b0f98b9890ef503092449c9363f42ecd347 (patch) | |
| tree | 5721fbfba92232aca633b30999d0311387055648 | |
| parent | 630e1d8c8b8652406e453309ba8d01fce3e3e72f (diff) | |
Equality: generic equality on constr replaced by eq_constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14328 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 21e593547c..de2a0dacf0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1396,8 +1396,8 @@ exception FoundHyp of (identifier * constr * bool) let is_eq_x gl x (id,_,c) = try let (_,lhs,rhs) = snd (find_eq_data_decompose gl c) in - if (x = lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); - if (x = rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) + if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true)); + if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false)) with PatternMatchingFailure -> () |