diff options
| author | Gaëtan Gilbert | 2018-09-19 14:21:37 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | 34f2cee9142fbd5df04fb1c63719de96609c1579 (patch) | |
| tree | 5333798acfdc2006b40a0e1333a5ca2a3b4ee017 /vernac/attributes.mli | |
| parent | c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd (diff) | |
Remove location field from attributes
It was never set, because it makes no sense.
Diffstat (limited to 'vernac/attributes.mli')
| -rw-r--r-- | vernac/attributes.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 571f0ddd7d..b8dcde5655 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -13,7 +13,6 @@ 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; @@ -21,6 +20,6 @@ type t = { deprecated : deprecation option; } -val mk_atts : ?loc: Loc.t option -> ?locality: bool option -> +val mk_atts : ?locality: bool option -> ?polymorphic: bool -> ?template:bool option -> ?program: bool -> ?deprecated: deprecation option -> unit -> t |