[vernac] attribute_of_flags

Elaborate a [atts] record out of a list of flags.

2 files changed, 25 insertions, 21 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5fda1a0da..135141cd4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2319,32 +2319,32 @@ let with_fail st b f =
       | _ -> assert false
   end
 
+let attributes_of_flags f atts =
+  List.fold_left
+    (fun (polymorphism, atts) f ->
+       match f with
+       | VernacProgram when not atts.program ->
+         (polymorphism, { atts with program = true })
+       | VernacProgram ->
+         user_err Pp.(str "Program mode specified twice")
+       | VernacPolymorphic b when polymorphism = None ->
+         (Some b, atts)
+       | VernacPolymorphic _ ->
+         user_err Pp.(str "Polymorphism specified twice")
+       | VernacLocal b when Option.is_empty atts.locality ->
+         (polymorphism, { atts with locality = Some b })
+       | VernacLocal _ ->
+         user_err Pp.(str "Locality specified twice")
+    )
+    (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
-  let flags f atts =
-    List.fold_left
-      (fun (polymorphism, atts) f ->
-         match f with
-         | VernacProgram when not atts.program ->
-           (polymorphism, { atts with program = true })
-         | VernacProgram ->
-           user_err Pp.(str "Program mode specified twice")
-         | VernacPolymorphic b when polymorphism = None ->
-           (Some b, atts)
-         | VernacPolymorphic _ ->
-           user_err Pp.(str "Polymorphism specified twice")
-         | VernacLocal b when Option.is_empty atts.locality ->
-           (polymorphism, { atts with locality = Some b })
-         | VernacLocal _ ->
-           user_err Pp.(str "Locality specified twice")
-      )
-      (None, atts)
-      f
-  in
   let rec control = function
   | VernacExpr (f, v) ->
-    let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+    let (polymorphism, atts) = attributes_of_flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
     aux ~polymorphism ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 02a3b2bd6..79f9b602a 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -38,3 +38,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 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_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts