3 files changed, 48 insertions, 37 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index eff666c9c..c0a6e5906 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -189,8 +189,7 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
   let nb_decls = List.length needed_levels + 1 in
   List.iter (prepare_empty_levels forpat) needed_levels;
-  unsafe_grammar_extend entry reinit (Option.map of_coq_position pos,
-    [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
+  unsafe_grammar_extend entry reinit (pos, [(name, p4assoc, [symbs, mkact pt])]);
   nb_decls) 0 rules
 
 type notation_grammar = {
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 8c8272589..70bcf1def 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -135,7 +135,18 @@ module Gram =
 
 (** This extension command is used by the Grammar constr *)
 
-let unsafe_grammar_extend e reinit ext =
+type unsafe_single_extend_statment =
+  string option *
+  gram_assoc option *
+  Gram.production_rule list
+
+type unsafe_extend_statment =
+  gram_position option *
+  unsafe_single_extend_statment list
+
+let unsafe_grammar_extend e reinit (pos, st) =
+  let map_s (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, rule) in
+  let ext =  (Option.map of_coq_position pos, List.map map_s st) in
   camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
   camlp4_verbose (maybe_uncurry (G.extend e)) ext
 
@@ -706,10 +717,10 @@ let of_coq_production_rule : type a. a Extend.production_rule -> _ = function
 | Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act)
 
 let of_coq_single_extend_statement (lvl, assoc, rule) =
-  (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule)
+  (lvl, assoc, List.map of_coq_production_rule rule)
 
 let of_coq_extend_statement (pos, st) =
-  (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st)
+  (pos, List.map of_coq_single_extend_statement st)
 
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8c3c299ad..372350414 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -96,28 +96,11 @@ module Gram : Compat.GrammarSig
 
 *)
 
-val gram_token_of_token : Tok.t -> Gram.symbol
-val gram_token_of_string : string -> Gram.symbol
-
-(** The superclass of all grammar entries *)
-type grammar_object
+(** {5 Grammar extension API} *)
 
 (** Type of reinitialization data *)
 type gram_reinit = gram_assoc * gram_position
 
-(** General entry keys *)
-
-(** This intermediate abstract representation of entries can
-   both be reified into mlexpr for the ML extensions and
-   dynamically interpreted as entries for the Coq level extensions
-*)
-
-(** Add one extension at some camlp4 position of some camlp4 entry *)
-val unsafe_grammar_extend :
-  grammar_object Gram.entry ->
-  gram_reinit option (** for reinitialization if ever needed *) ->
-  Gram.extend_statment -> unit
-
 val grammar_extend :
   'a Gram.entry ->
   gram_reinit option (** for reinitialization if ever needed *) ->
@@ -251,17 +234,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry
 val get_command_entry : unit -> vernac_expr Gram.entry
 val set_command_entry : vernac_expr Gram.entry -> unit
 
-(** Mapping formal entries into concrete ones *)
-
-(** Binding constr entry keys to entries and symbols *)
-
-val interp_constr_entry_key : bool (** true for cases_pattern *) ->
-  int -> grammar_object Gram.entry * int option
-
-val symbol_of_constr_prod_entry_key : gram_assoc option ->
-  constr_entry_key -> bool -> constr_prod_entry_key ->
-    Gram.symbol
-
 val name_of_entry : 'a Gram.entry -> 'a Entry.t
 
 val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option
@@ -287,9 +259,38 @@ val register_empty_levels : bool -> int list ->
 
 val remove_levels : int -> unit
 
+(** {5 Unsafe grammar extension API}
+
+For compatibility purpose only. Do not use in newly written code.
+
+*)
+
+val gram_token_of_token : Tok.t -> Gram.symbol
+val gram_token_of_string : string -> Gram.symbol
 val level_of_snterml : Gram.symbol -> int
 
-(** TODO: remove me *)
+(** The superclass of all grammar entries *)
+type grammar_object
+
+(** Binding constr entry keys to entries and symbols *)
+
+val interp_constr_entry_key : bool (** true for cases_pattern *) ->
+  int -> grammar_object Gram.entry * int option
+
+val symbol_of_constr_prod_entry_key : gram_assoc option ->
+  constr_entry_key -> bool -> constr_prod_entry_key ->
+    Gram.symbol
 
-val of_coq_position :  Extend.gram_position -> Compat.CompatGramext.position
-val of_coq_assoc :  Extend.gram_assoc -> Compat.CompatGramext.assoc
+type unsafe_single_extend_statment =
+  string option *
+  gram_assoc option *
+  Gram.production_rule list
+
+type unsafe_extend_statment =
+  gram_position option *
+  unsafe_single_extend_statment list
+
+val unsafe_grammar_extend :
+  grammar_object Gram.entry ->
+  gram_reinit option (** for reinitialization if ever needed *) ->
+  unsafe_extend_statment -> unit