diff options
| author | Gaëtan Gilbert | 2018-09-19 14:33:44 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | a9f2ba45c7dba54bfd44078587fc6176a5af68d6 (patch) | |
| tree | 0c967bedf93837d3844f8fe831043c6b58d000fa | |
| parent | 80785aee7924309ab21b8ce1dcf7964559531216 (diff) | |
Remove pointless optional arguments to mk_atts
| -rw-r--r-- | vernac/attributes.ml | 12 | ||||
| -rw-r--r-- | vernac/attributes.mli | 6 |
2 files changed, 13 insertions, 5 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index ce77256edd..c93ff2a63a 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -24,8 +24,16 @@ type t = { deprecated : deprecation option; } -let mk_atts ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () = - { locality ; polymorphic ; program ; deprecated; template } +let default = { + locality = None; + polymorphic = false; + template = None; + program = false; + deprecated = None; +} + +let mk_atts ?(polymorphic=default.polymorphic) ?(program=default.program) () = + { default with polymorphic; program } let attributes_of_flags f atts = let assert_empty k v = diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 7fe71bb048..b9191c3f3e 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -20,9 +20,9 @@ type t = { deprecated : deprecation option; } -val mk_atts : ?locality: bool option -> - ?polymorphic: bool -> ?template:bool option -> - ?program: bool -> ?deprecated: deprecation option -> unit -> t +val mk_atts : + ?polymorphic: bool -> + ?program: bool -> unit -> t val attributes_of_flags : Vernacexpr.vernac_flags -> t -> bool option (* polymorphism attr *) * t |