diff options
| author | Maxime Dénès | 2017-12-29 13:43:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-29 13:43:28 +0100 |
| commit | 3624d943513ff1d79fdadf5b231ffcd3786b16c8 (patch) | |
| tree | 6bfd3884ff693eb7bfe5abd3dfc21c537eb5f1ea /plugins/ltac/rewrite.ml | |
| parent | c0e5746e6b273eb4592d24867da55dde40b656c9 (diff) | |
| parent | 1e1d8d67442dc3cdd248b7f5e027b9d6bf998ba3 (diff) | |
Merge PR #6405: Remove the local polymorphic flag hack.
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a698b05dd7..3cbb110010 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1981,8 +1981,7 @@ let add_morphism_infer glob m n = Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob - poly (ConstRef cst)); + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else let kind = Decl_kinds.Global, poly, @@ -1993,7 +1992,7 @@ let add_morphism_infer glob m n = | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info - glob poly (ConstRef cst)); + glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false in |