diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -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 |