[parsing] Move pcoq-specific parts in extend to pcoq.

3 files changed, 27 insertions, 14 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 63e121c0d1..8dc77e1216 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -79,6 +79,8 @@ type ('a,'b,'c) ty_user_symbol =
 
 (** {5 Type-safe grammar extension} *)
 
+(* Should be merged with gramlib's implementation *)
+
 type norec = NoRec    (* just two *)
 type mayrec = MayRec  (* incompatible types *)
 
@@ -107,15 +109,3 @@ and 'a rules =
 
 type 'a production_rule =
 | Rule : ('a, _, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
-
-type 'a single_extend_statement =
-  string option *
-  (* Level *)
-  Gramlib.Gramext.g_assoc option *
-  (* Associativity *)
-  'a production_rule list
-  (* Symbol list with the interpretation function *)
-
-type 'a extend_statement =
-  Gramlib.Gramext.position option *
-  'a single_extend_statement list
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 3aaba27579..fa837c484c 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -215,6 +215,18 @@ let fix_extend_statement (pos, st) =
 (** Type of reinitialization data *)
 type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 
+type 'a single_extend_statement =
+  string option *
+  (* Level *)
+  Gramlib.Gramext.g_assoc option *
+  (* Associativity *)
+  'a production_rule list
+  (* Symbol list with the interpretation function *)
+
+type 'a extend_statement =
+  Gramlib.Gramext.position option *
+  'a single_extend_statement list
+
 type extend_rule =
 | ExtendRule : 'a G.Entry.e * gram_reinit option * 'a extend_statement -> extend_rule
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7efeab6ba0..10f78a5a72 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -212,8 +212,19 @@ val epsilon_value : ('a -> 'self) -> ('self, _, 'a) Extend.symbol -> 'self optio
 type gram_reinit = Gramlib.Gramext.g_assoc * Gramlib.Gramext.position
 (** Type of reinitialization data *)
 
-val grammar_extend : 'a Entry.t -> gram_reinit option ->
-  'a Extend.extend_statement -> unit
+type 'a single_extend_statement =
+  string option *
+  (* Level *)
+  Gramlib.Gramext.g_assoc option *
+  (* Associativity *)
+  'a production_rule list
+  (* Symbol list with the interpretation function *)
+
+type 'a extend_statement =
+  Gramlib.Gramext.position option *
+  'a single_extend_statement list
+
+val grammar_extend : 'a Entry.t -> gram_reinit option -> 'a extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)