{Vernacentries -> Attributes}.attributes_of_flags

5 files changed, 65 insertions, 63 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index b393093601..037c63ef03 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,7 +194,7 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let _, atts = Vernacentries.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in
+      let _, atts = Attributes.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in
       let poly = atts.Attributes.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 2bef6ff320..ce77256edd 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -8,6 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open CErrors
+open Vernacexpr
+
 type deprecation = { since : string option ; note : string option }
 
 let mk_deprecation ?(since=None) ?(note=None) () =
@@ -23,3 +26,61 @@ type t = {
 
 let mk_atts ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () =
   { locality ; polymorphic ; program ; deprecated; template }
+
+let attributes_of_flags f atts =
+  let assert_empty k v =
+    if v <> VernacFlagEmpty
+    then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+  in
+  List.fold_left
+    (fun (polymorphism, atts) (k, v) ->
+       match k with
+       | "program" when not atts.program ->
+         assert_empty k v;
+         (polymorphism, { atts with program = true })
+       | "program" ->
+         user_err Pp.(str "Program mode specified twice")
+       | "polymorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some true, atts)
+       | "monomorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some false, atts)
+       | ("polymorphic" | "monomorphic") ->
+         user_err Pp.(str "Polymorphism specified twice")
+       | "template" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some true }
+       | "notemplate" when atts.template = None ->
+         assert_empty k v;
+         polymorphism, { atts with template = Some false }
+       | "template" | "notemplate" ->
+         user_err Pp.(str "Templateness specified twice")
+       | "local" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some true })
+       | "global" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some false })
+       | ("local" | "global") ->
+         user_err Pp.(str "Locality specified twice")
+       | "deprecated" when Option.is_empty atts.deprecated ->
+           begin match v with
+             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
+             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+               let since = Some since and note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
+             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+               let since = Some since in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
+             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+               let note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
+             |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+           end
+       | "deprecated" ->
+         user_err Pp.(str "Deprecation specified twice")
+       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
+    )
+    (None, atts)
+    f
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index b8dcde5655..7fe71bb048 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -23,3 +23,6 @@ type t = {
 val mk_atts : ?locality: bool option ->
   ?polymorphic: bool -> ?template:bool option ->
   ?program: bool -> ?deprecated: deprecation option -> unit -> t
+
+val attributes_of_flags : Vernacexpr.vernac_flags -> t ->
+  bool option (* polymorphism attr *) * t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 57585f11c7..12feb07051 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2370,64 +2370,6 @@ let with_fail st b f =
       | _ -> assert false
   end
 
-let attributes_of_flags f atts =
-  let assert_empty k v =
-    if v <> VernacFlagEmpty
-    then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
-  in
-  List.fold_left
-    (fun (polymorphism, atts) (k, v) ->
-       match k with
-       | "program" when not atts.program ->
-         assert_empty k v;
-         (polymorphism, { atts with program = true })
-       | "program" ->
-         user_err Pp.(str "Program mode specified twice")
-       | "polymorphic" when polymorphism = None ->
-         assert_empty k v;
-         (Some true, atts)
-       | "monomorphic" when polymorphism = None ->
-         assert_empty k v;
-         (Some false, atts)
-       | ("polymorphic" | "monomorphic") ->
-         user_err Pp.(str "Polymorphism specified twice")
-       | "template" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some true }
-       | "notemplate" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some false }
-       | "template" | "notemplate" ->
-         user_err Pp.(str "Templateness specified twice")
-       | "local" when Option.is_empty atts.locality ->
-         assert_empty k v;
-         (polymorphism, { atts with locality = Some true })
-       | "global" when Option.is_empty atts.locality ->
-         assert_empty k v;
-         (polymorphism, { atts with locality = Some false })
-       | ("local" | "global") ->
-         user_err Pp.(str "Locality specified twice")
-       | "deprecated" when Option.is_empty atts.deprecated ->
-           begin match v with
-             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
-             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-               let since = Some since and note = Some note in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
-             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
-               let since = Some since in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
-             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
-               let note = Some note in
-               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
-             |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
-           end
-       | "deprecated" ->
-         user_err Pp.(str "Deprecation specified twice")
-       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
-    )
-    (None, atts)
-    f
-
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f533dd25f4..f95bdaa539 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -39,10 +39,6 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 
 val universe_polymorphism_option_name : string list
 
-(** Elaborate a [atts] record out of a list of flags.
-    Also returns whether polymorphism is explicitly (un)set. *)
-val attributes_of_flags : Vernacexpr.vernac_flags -> Attributes.t -> bool option * Attributes.t
-
 (** {5 VERNAC EXTEND} *)
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification