diff options
| author | Gaëtan Gilbert | 2018-11-06 13:59:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-05 13:21:18 +0100 |
| commit | 90ae85437a281ca655f7e9511ef09874ba591857 (patch) | |
| tree | 8dc0284f3c2af00b3ed0c01562bc64ee43b59d3c /vernac/attributes.ml | |
| parent | 33de5194171ad547864a7c3d6489498ddb53e562 (diff) | |
Move template out of Defattributes record
Diffstat (limited to 'vernac/attributes.ml')
| -rw-r--r-- | vernac/attributes.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 9ab8f7c8fd..4f238f38e6 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -173,10 +173,9 @@ let polymorphic_nowarn = universe_transform ~warn_unqualified:false >> qualify_attribute ukey polymorphic_base -let universe_poly_template = - let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in +let template = universe_transform ~warn_unqualified:true >> - qualify_attribute ukey (polymorphic_base ++ template) + qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") let polymorphic = universe_transform ~warn_unqualified:true >> |