Getting rid of most uses of unsafe_grammar_extend.

3 files changed, 13 insertions, 40 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 14fe15e89..84736f8ab 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -167,10 +167,9 @@ let rec make_constr_prod_item assoc from forpat = function
       []
 
 let prepare_empty_levels forpat (pos,p4assoc,name,reinit) =
-  let entry =
-    if forpat then weaken_entry Constr.pattern
-    else weaken_entry Constr.operconstr in
-  unsafe_grammar_extend entry reinit (pos,[(name, p4assoc, [])])
+  let empty = (pos, [(name, p4assoc, [])]) in
+  if forpat then grammar_extend Constr.pattern reinit empty
+  else grammar_extend Constr.operconstr reinit empty
 
 let pure_sublevels level symbs =
   let filter s =
@@ -189,9 +188,6 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   let symbs = make_constr_prod_item assoc n forpat pt in
   let pure_sublevels = pure_sublevels level symbs in
   let needed_levels = register_empty_levels forpat pure_sublevels in
-  let map_level (pos, ass1, name, ass2) =
-    (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in
-  let needed_levels = List.map map_level needed_levels in
   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;
@@ -233,11 +229,11 @@ let extend_constr_notation ng =
 
 let get_tactic_entry n =
   if Int.equal n 0 then
-    weaken_entry Tactic.simple_tactic, None
+    Tactic.simple_tactic, None
   else if Int.equal n 5 then
-    weaken_entry Tactic.binder_tactic, None
+    Tactic.binder_tactic, None
   else if 1<=n && n<5 then
-    weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
+    Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
   else
     error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
 
@@ -257,7 +253,7 @@ type all_grammar_command =
 (** ML Tactic grammar extensions *)
 
 let add_ml_tactic_entry name prods =
-  let entry = weaken_entry Tactic.simple_tactic in
+  let entry = Tactic.simple_tactic in
   let mkact i loc l : raw_tactic_expr =
     let open Tacexpr in
     let entry = { mltac_name = name; mltac_index = i } in
@@ -265,7 +261,7 @@ let add_ml_tactic_entry name prods =
   in
   let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in
   synchronize_level_positions ();
-  unsafe_grammar_extend entry None (None ,[(None, None, List.rev rules)]);
+  grammar_extend entry None (None, [(None, None, List.rev rules)]);
   1
 
 (* Declaration of the tactic grammar rule *)
@@ -285,7 +281,7 @@ let add_tactic_entry kn tg =
   in
   let rules = make_rule mkact tg.tacgram_prods in
   synchronize_level_positions ();
-  unsafe_grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
+  grammar_extend entry None (pos, [(None, None, List.rev [rules])]);
   1
 
 let (grammar_state : (int * all_grammar_command) list ref) = ref []
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 96c1566c4..7a66b24f3 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -13,19 +13,6 @@ open Pcoq
 open Genarg
 open Vernacexpr
 
-(** Making generic actions in type generic_argument *)
-
-let make_generic_action
-  (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
-  let rec make env = function
-    | [] ->
-	Gram.action (fun loc -> f (to_coqloc loc) env)
-    | None :: tl -> (* parse a non-binding item *)
-        Gram.action (fun _ -> make env tl)
-    | Some (p, t) :: tl -> (* non-terminal *)
-        Gram.action (fun v -> make ((p, Unsafe.inj t v) :: env) tl) in
-  make [] (List.rev pil)
-
 (** Grammar extensions declared at ML level *)
 
 type 's grammar_prod_item =
@@ -33,16 +20,6 @@ type 's grammar_prod_item =
   | GramNonTerminal :
       Loc.t * argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item
 
-let make_prod_item = function
-  | GramTerminal s -> (gram_token_of_string s, None)
-  | GramNonTerminal (_,t,e,po) ->
-      (symbol_of_prod_entry_key e, Option.map (fun p -> (p,t)) po)
-
-let make_rule mkact pt =
-  let (symbs,ntl) = List.split (List.map make_prod_item pt) in
-  let act = make_generic_action mkact ntl in
-  (symbs, act)
-
 type 'a ty_arg = Id.t * ('a -> raw_generic_argument)
 
 type ('self, _, 'r) ty_rule =
@@ -84,7 +61,7 @@ let rec ty_eval : type s a r. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> a = fu
   let f loc args = f loc ((id, inj x) :: args) in
   ty_eval rem f
 
-let make_rule' f prod =
+let make_rule f prod =
   let AnyTyRule ty_rule = ty_rule_of_gram (List.rev prod) in
   let symb = ty_erase ty_rule in
   let f loc l = f loc (List.rev l) in
@@ -107,5 +84,5 @@ let extend_vernac_command_grammar s nt gl =
   let nt = Option.default Vernac_.command nt in
   vernac_exts := (s,gl) :: !vernac_exts;
   let mkact loc l = VernacExtend (s,List.map snd l) in
-  let rules = [make_rule' mkact gl] in
+  let rules = [make_rule mkact gl] in
   grammar_extend nt None (None, [None, None, rules])
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 182a72086..32646cfaf 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -27,5 +27,5 @@ val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
-  (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) ->
-  's grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
+  (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'a) ->
+  'a grammar_prod_item list -> 'a Extend.production_rule