diff options
| author | Gaëtan Gilbert | 2018-09-19 14:14:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd (patch) | |
| tree | 7f9a76cc9119a094e6b551e5d982ca46a81e013b /vernac/vernacinterp.mli | |
| parent | 9b0a4b002e324d523b01e17fba7ba631a651f6b0 (diff) | |
Move attributes out of vernacinterp to new attributes module
Diffstat (limited to 'vernac/vernacinterp.mli')
| -rw-r--r-- | vernac/vernacinterp.mli | 21 |
1 files changed, 2 insertions, 19 deletions
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 |