diff options
| author | Gaëtan Gilbert | 2020-02-06 20:25:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 6283c94c640d6b1f911b644583ee656a7a8b9a1f (patch) | |
| tree | 9d1c95a5b38fd6485bc8d8f9de2f2b30a8f542a0 /plugins | |
| parent | b8fb594259f7abaedc4e335cfd8eacd0508fffcf (diff) | |
unsafe_type_of -> get_type_of in Rewrite.default_morphism
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a52d03c57a..2a1f85b13f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1937,7 +1937,7 @@ let build_morphism_signature env sigma m = let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in |