Further reducing the dependencies of the EXTEND macros.

5 files changed, 22 insertions, 45 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index bebde706e..801229bcb 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -16,11 +16,6 @@ open Extend
 let loc = CompatLoc.ghost
 let default_loc = <:expr< Loc.ghost >>
 
-let qualified_name loc s =
-  let path = CString.split '.' s in
-  let (name, path) = CList.sep_last path in
-  qualified_name loc path name
-
 let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
@@ -56,7 +51,7 @@ let make_rule loc (prods,act) =
   <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >>
 
 let is_ident x = function
-| <:expr< $lid:s$ >> -> CString.equal s x
+| <:expr< $lid:s$ >> -> (s : string) = x
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
@@ -85,7 +80,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let glob = match g with
     | None ->
       begin match rawtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun ist v -> (ist, v) >>
       | _ ->
         <:expr< fun ist v ->
@@ -100,7 +95,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let interp = match f with
     | None ->
       begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun ist v -> Ftactic.return v >>
       | _ ->
 	<:expr< fun ist x ->
@@ -120,7 +115,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let subst = match h with
     | None ->
       begin match globtyp with
-      | Genarg.ExtraArgType s' when CString.equal s s' ->
+      | Genarg.ExtraArgType s' when s = s' ->
         <:expr< fun s v -> v >>
       | _ ->
         <:expr< fun s x ->
@@ -132,7 +127,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let dyn = match typ with
   | `Uniform typ ->
     let is_new = match typ with
-    | Genarg.ExtraArgType s' when CString.equal s s' -> true
+    | Genarg.ExtraArgType s' when s = s' -> true
     | _ -> false
     in
     if is_new then <:expr< None >>
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 42fc73878..9b24c9797 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,15 +1,8 @@
 Coq_config
 
-Hashset
-Hashcons
-CMap
-Int
-Option
 Store
 Exninfo
 Loc
-CList
-CString
 
 Tok
 Compat
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index d91bfd7b8..bde1e7651 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -57,7 +57,7 @@ let rec mlexpr_of_prod_entry_key f = function
   | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >>
   | Extend.Uentryl (e, l) ->
     (** Keep in sync with Pcoq! *)
-    assert (CString.equal e "tactic");
+    assert (e = "tactic");
     if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >>
     else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >>
 
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 1951b8b45..a34b880ae 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -24,15 +24,6 @@ let rec make_patt = function
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
-let rec mlexpr_of_argtype loc = function
-  | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
-  | Genarg.PairArgType (t1,t2) ->
-      let t1 = mlexpr_of_argtype loc t1 in
-      let t2 = mlexpr_of_argtype loc t2 in
-      <:expr< Genarg.PairArgType $t1$ $t2$ >>
-  | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >>
-
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
   | ExtNonTerminal (t, _, p) :: l ->
@@ -44,12 +35,6 @@ let rec make_let raw e = function
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let raw e l
 
-let rec extract_signature = function
-  | [] -> []
-  | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l
-  | _::l -> extract_signature l
-
-
 let make_clause (pt,_,e) =
   (make_patt pt,
    vala None,
@@ -99,13 +84,13 @@ let declare_tactic loc s c cl = match cl with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in
   let name = mlexpr_of_string name in
-  let tac =
+  let tac = match rem with
+  | [] ->
     (** Special handling of tactics without arguments: such tactics do not do
         a Proofview.Goal.nf_enter to compute their arguments. It matters for some
         whole-prof tactics like [shelve_unifiable]. *)
-    if CList.is_empty rem then
       <:expr< fun _ $lid:"ist"$ -> $tac$ >>
-    else
+  | _ ->
       let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
       <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
   in
@@ -178,7 +163,7 @@ EXTEND
         let e = parse_user_entry e sep in
         ExtNonTerminal (type_of_user_symbol e, e, s)
       | s = STRING ->
-	let () = if CString.is_empty s then failwith "Empty terminal." in
+	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
     ] ]
   ;
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 453907689..40e327c37 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -43,9 +43,11 @@ 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 p
-  | _ -> None) pt in
+  let fold accu = function
+  | ExtNonTerminal (_, _, p) -> p :: accu
+  | _ -> accu
+  in
+  let names = List.fold_left fold [] pt in
   let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
@@ -99,10 +101,12 @@ let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
-let mlexpr_of_clause =
-  mlexpr_of_list
-    (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item
-       (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b))
+let mlexpr_of_clause cl =
+  let mkexpr { r_head = a; r_patt = b; } = match a with
+  | None -> mlexpr_of_list make_prod_item b
+  | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b)
+  in
+  mlexpr_of_list mkexpr cl
 
 let declare_command loc s c nt cl =
   let se = mlexpr_of_string s in
@@ -160,7 +164,7 @@ EXTEND
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
         d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
-      let () = if CString.is_empty s then failwith "Command name is empty." in
+      let () = if s = "" then failwith "Command name is empty." in
       let b = <:expr< fun () -> $e$ >> in
       { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;