diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /stm | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
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 6ad1294fc..794fabc91 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 bc0c0c2b3..329c90198 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 |