diff options
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 1f68117a76..c5ed02e043 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -453,7 +453,7 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = Typing.unsafe_type_of env sigma e1 in (t,e1,e2) + let t = Retyping.get_type_of env sigma e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) |