Reducing the number of modules linked in grammar.cma.

6 files changed, 15 insertions, 27 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 65dc237bb..be4097f13 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -82,21 +82,19 @@ let statically_known_possibly_empty s (prods,_) =
       prods
 
 let possibly_empty_subentries loc (prods,act) =
-  let bind_name id v e =
-    let s = Names.Id.to_string id in
+  let bind_name s v e =
     <:expr< let $lid:s$ = $v$ in $e$ >>
   in
   let rec aux = function
     | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
-    | ExtNonTerminal(_, e, id) :: tl when is_possibly_empty e ->
-        bind_name id (get_empty_entry e) (aux tl)
-    | ExtNonTerminal(t, _, id) :: tl ->
+    | ExtNonTerminal(_, e, s) :: tl when is_possibly_empty e ->
+        bind_name s (get_empty_entry e) (aux tl)
+    | ExtNonTerminal(t, _, s) :: tl ->
         let t = match t with
         | ExtraArgType _ as t -> t
         | _ -> assert false
         in
         (* We check at runtime if extraarg s parses "epsilon" *)
-        let s = Names.Id.to_string id in
         <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
           [ None -> raise Exit
           | Some v -> v ] in $aux tl$ >>
@@ -130,7 +128,6 @@ let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
     | ExtNonTerminal (t, _, p) :: tl ->
-	let p = Names.Id.to_string p in
 	<:expr<
             (fun $lid:p$ ->
                let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
@@ -312,10 +309,10 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
 	  if String.length s > 0 && Util.is_letter s.[0] then
 	    Lexer.add_keyword s;
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 296d32dc0..6a265bf4a 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -2,7 +2,6 @@ Coq_config
 
 Hook
 Terminal
-Canary
 Hashset
 Hashcons
 CSet
@@ -29,14 +28,11 @@ CStack
 Util
 Ppstyle
 Errors
-Predicate
 Segmenttree
 Unicodetable
 Unicode
 Genarg
 
-Names
-
 Stdarg
 Constrarg
 
@@ -47,7 +43,6 @@ Entry
 Pcoq
 
 Q_util
-Egramml
 Argextend
 Tacextend
 Vernacextend
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index c6e2e9966..f013e323e 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -13,7 +13,7 @@ open Compat
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t
+| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
 
 let mlexpr_of_list f l =
   List.fold_right
@@ -55,7 +55,7 @@ let mlexpr_of_option f = function
   | Some e -> <:expr< Some $f e$ >>
 
 let mlexpr_of_ident id =
-  <:expr< Names.Id.of_string $str:Names.Id.to_string id$ >>
+  <:expr< Names.Id.of_string $str:id$ >>
 
 let mlexpr_of_token = function
 | Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >>
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index d0e0dab22..90fe1645f 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -10,7 +10,7 @@ open Compat (* necessary for camlp4 *)
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * Names.Id.t
+| ExtNonTerminal of Genarg.argument_type * Extend.user_symbol * string
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
@@ -34,7 +34,7 @@ val mlexpr_of_string : string -> MLast.expr
 
 val mlexpr_of_option : ('a -> MLast.expr) -> 'a option -> MLast.expr
 
-val mlexpr_of_ident : Names.Id.t -> MLast.expr
+val mlexpr_of_ident : string -> MLast.expr
 
 val mlexpr_of_prod_entry_key : Extend.user_symbol -> MLast.expr
 
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 10afcdd21..c35fa00d2 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -27,7 +27,6 @@ let plugin_name = <:expr< __coq_plugin_name >>
 let rec make_patt = function
   | [] -> <:patt< [] >>
   | ExtNonTerminal (_, _, p) :: l ->
-      let p = Names.Id.to_string p in
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
@@ -43,7 +42,6 @@ let rec mlexpr_of_argtype loc = function
 let rec make_when loc = function
   | [] -> <:expr< True >>
   | ExtNonTerminal (t, _, p) :: l ->
-      let p = Names.Id.to_string p in
       let l = make_when loc l in
       let t = mlexpr_of_argtype loc t in
       <:expr< Genarg.argument_type_eq (Genarg.genarg_tag $lid:p$) $t$ && $l$ >>
@@ -52,7 +50,6 @@ let rec make_when loc = function
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | ExtNonTerminal (t, _, p) :: l ->
-      let p = Names.Id.to_string p in
       let loc = MLast.loc_of_expr e in
       let e = make_let raw e l in
       let v =
@@ -198,10 +195,10 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
 	if String.is_empty s then Errors.user_err_loc (!@loc,"",Pp.str "Empty terminal.");
         ExtTerminal s
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 57079fccd..3bb1e0907 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -35,7 +35,6 @@ type rule = {
 let rec make_let e = function
   | [] -> e
   | ExtNonTerminal (t, _, p) :: l ->
-      let p = Names.Id.to_string p in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
       <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
@@ -49,7 +48,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
 (* To avoid warnings *)
 let mk_ignore c pt =
   let names = CList.map_filter (function
-  | ExtNonTerminal (_, _, p) -> Some (Names.Id.to_string p)
+  | ExtNonTerminal (_, _, p) -> Some p
   | _ -> None) pt in
   let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
   let names = List.fold_left fold <:expr< () >> names in
@@ -181,10 +180,10 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (type_of_user_symbol e, e, Names.Id.of_string s)
+        ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
         ExtTerminal s
     ] ]