diff options
| -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 -> () |