Move attributes out of vernacinterp to new attributes module

7 files changed, 60 insertions, 41 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
new file mode 100644
index 0000000000..2f1f6e04e3
--- /dev/null
+++ b/vernac/attributes.ml
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type deprecation = { since : string option ; note : string option }
+
+let mk_deprecation ?(since=None) ?(note=None) () =
+  { since ; note }
+
+type t = {
+  loc : Loc.t option;
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  program : bool;
+  deprecated : deprecation option;
+}
+
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () =
+  { loc ; locality ; polymorphic ; program ; deprecated; template }
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
new file mode 100644
index 0000000000..571f0ddd7d
--- /dev/null
+++ b/vernac/attributes.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type deprecation = { since : string option ; note : string option }
+
+val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
+
+type t = {
+  loc : Loc.t option;
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  program : bool;
+  deprecated : deprecation option;
+}
+
+val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+  ?polymorphic: bool -> ?template:bool option ->
+  ?program: bool -> ?deprecated: deprecation option -> unit -> t
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 356951b695..35ce8c726b 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -7,6 +7,7 @@ Himsg
 ExplainErr
 Locality
 Egramml
+Attributes
 Vernacinterp
 Ppvernac
 Proof_using
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1190d73258..391e8f7990 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -31,6 +31,7 @@ open Redexpr
 open Lemmas
 open Locality
 open Vernacinterp
+open Attributes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -2109,7 +2110,6 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
-  let open Vernacinterp in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
@@ -2505,7 +2505,7 @@ open Extend
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 0c4630e45f..f533dd25f4 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,14 +41,14 @@ 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 -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+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
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 2746cbd144..b16784eb22 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,24 +12,7 @@ open Util
 open Pp
 open CErrors
 
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
-  { since ; note }
-
-type atts = {
-  loc : Loc.t option;
-  locality : bool option;
-  polymorphic : bool;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
-  { loc ; locality ; polymorphic ; program ; deprecated; template }
-
-type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 62a178b555..ba3d911810 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,24 +10,7 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
-type atts = {
-  loc : Loc.t option;
-  locality : bool option;
-  polymorphic : bool;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?template:bool option ->
-  ?program: bool -> ?deprecated: deprecation option -> unit -> atts
-
-type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -35,4 +18,4 @@ val vinterp_init : unit -> unit
 val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t