aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/vernac_classifier.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/vernac_classifier.mli')
-rw-r--r--stm/vernac_classifier.mli2
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