diff options
| author | Gaëtan Gilbert | 2020-02-06 20:22:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | b8fb594259f7abaedc4e335cfd8eacd0508fffcf (patch) | |
| tree | 672557a7dda635f9318e24dff1dc64eda044648a | |
| parent | 791797fce5e11b83b88e6b869678ee7c39703043 (diff) | |
unsafe_type_of -> type_of in Rewrite.build_morphism_signature
| -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 7cb359b8cd..a52d03c57a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1907,7 +1907,7 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in - let t = Typing.unsafe_type_of env sigma m in + let t = Retyping.get_type_of env sigma m in let cstrs = let rec aux t = match EConstr.kind sigma t with |