diff options
| author | Gaëtan Gilbert | 2020-02-06 16:07:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | d584d0643e32f2277b1a38ba46fc92993638492b (patch) | |
| tree | 4cbf55a3db010a8eadbb3bd50a01e0ed85eca2ed | |
| parent | 34d95672ecace6733d9d2f738ee6d7aee46fb2d0 (diff) | |
unsafe_type_of -> get_type_of in Hipattern.extract_eq_args
| -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) |