diff options
| author | Gaëtan Gilbert | 2020-02-06 16:29:29 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 907df42d15904c13b4e8c5af0e24ff0406b3f6ed (patch) | |
| tree | 1116c711e1f1c77f166478410c8119685d29d17e /tactics/autorewrite.ml | |
| parent | 50f5b99e9ffce8d7a54b1a35b899e0645df72632 (diff) | |
unsafe_type_of -> get_type_of in Autorewrite.{find,decompose}_applied_relation
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index cd6f445503..1bbcca8827 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -238,7 +238,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = in try let others,(c1,c2) = split_last_two args in - let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + let ty1, ty2 = Retyping.get_type_of env eqclause.evd c1, Retyping.get_type_of env eqclause.evd c2 in (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) let open EConstr in let hyp_ty = Unsafe.to_constr ty in @@ -261,7 +261,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation ?loc metas env sigma c left2right = - let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in + let ctype = Retyping.get_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> |