From edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 Sep 2014 22:13:08 +0200
Subject: VernacExtend does not dispatch on type anymore.

---
 intf/vernacexpr.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5bf83e2c19..b784bc4334 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -223,6 +223,8 @@ type section_subset_expr =
 
 type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
 
+type extend_name = string * int
+
 (* This type allows registering the inlining of constants in native compiler.
    It will be extended with primitive inductive types and operators *)
 type register_kind = 
@@ -427,7 +429,7 @@ type vernac_expr =
   | VernacToplevelControl of exn
 
   (* For extension *)
-  | VernacExtend of string * Genarg.raw_generic_argument list
+  | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
   (* Flags *)
   | VernacProgram of vernac_expr
-- 
cgit v1.2.3