diff options
| author | Gaëtan Gilbert | 2018-10-11 18:12:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | 1b753da49ea4a10d7779bb50d93bea25157c01bd (patch) | |
| tree | 88fc18e1cfd69318258c6d69082fb883b80db3ff /vernac/attributes.mli | |
| parent | c7ce8a036e07930793dc4904457188ca97064700 (diff) | |
Load doesn't support attributes
Diffstat (limited to 'vernac/attributes.mli')
| -rw-r--r-- | vernac/attributes.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 7a75e9d922..27b873bfe0 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -19,6 +19,9 @@ type +'a attribute val parse : 'a attribute -> vernac_flags -> 'a (** Errors on unsupported attributes. *) +val unsupported_attributes : vernac_flags -> unit +(** Errors if the list of flags is nonempty. *) + module Notations : sig (** Notations to combine attributes. *) |