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/vernac_classifier.mli | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'stm/vernac_classifier.mli')
| -rw-r--r-- | stm/vernac_classifier.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |