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 | |
| parent | c7ce8a036e07930793dc4904457188ca97064700 (diff) | |
Load doesn't support attributes
| -rw-r--r-- | vernac/attributes.ml | 4 | ||||
| -rw-r--r-- | vernac/attributes.mli | 3 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
3 files changed, 8 insertions, 3 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 389441356e..14db90c3de 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -11,13 +11,13 @@ open CErrors open Vernacexpr -let unsupported_attributes ?loc = function +let unsupported_attributes = function | [] -> () | atts -> let keys = List.map fst atts in let keys = List.sort_uniq String.compare keys in let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in - user_err ?loc Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") + user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") type 'a key_parser = 'a option -> vernac_flag_value -> 'a 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. *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3bdca0cc9f..416351d76b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2398,7 +2398,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} = and aux ~atts : _ -> unit = function - | VernacLoad (_,fname) -> vernac_load control fname + | VernacLoad (_,fname) -> + Attributes.unsupported_attributes atts; + vernac_load control fname | c -> let poly, program = let open Attributes in |