diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e73a18b79..3433987e3 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1896,7 +1896,6 @@ 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 m = EConstr.of_constr m in let sigma = Evd.from_ctx ctx in let t = Typing.unsafe_type_of env sigma m in let cstrs = |