diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/vernac_classifier.ml | 4 | ||||
| -rw-r--r-- | stm/vernac_classifier.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 6ad1294fc3..794fabc910 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -37,7 +37,7 @@ let string_of_vernac_classification (t,w) = let classifiers = ref [] let declare_vernac_classifier - (s : string) + (s : Vernacexpr.extend_name) (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) = classifiers := !classifiers @ [s,f] @@ -201,7 +201,7 @@ let rec classify_vernac e = (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () - with Not_found -> anomaly(str"No classifier for"++spc()++str s) + with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) and classify_vernac_list = function (* spiwack: It would be better to define a monoid on classifiers. So that the classifier of the list would be the composition of diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index bc0c0c2b30..329c901988 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -16,7 +16,7 @@ val classify_vernac : vernac_expr -> vernac_classification (** Install a vernacular classifier for VernacExtend *) val declare_vernac_classifier : - string -> (raw_generic_argument list -> unit -> vernac_classification) -> unit + Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit (** Set by Stm *) val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit |