diff options
Diffstat (limited to 'tactics/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4b94f420..95f3af57 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_type_of gl e1 in (t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl t1 t2 then (t1,e1,e2) |