[camlpX] Remove camlp4 compat layer.

We remove the camlp4 compatibility layer, and try to clean up
most structures. `parsing/compat` is gone.

We added some documentation to the lexer/parser interfaces that are
often obscured by module includes.

8 files changed, 26 insertions, 156 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index d0ab5d803..aaf3afe43 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -7,11 +7,13 @@
 (************************************************************************)
 
 open Q_util
-open GramCompat
 
-let loc = CompatLoc.ghost
+let loc = Ploc.dummy
 let default_loc = <:expr< Loc.ghost >>
 
+let declare_str_items loc l =
+  MLast.StDcl (loc, Ploc.VaVal l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+
 let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
 
 let rec make_wit loc = function
@@ -185,7 +187,6 @@ let declare_vernac_argument loc s pr cl =
       >> ]
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;
diff --git a/grammar/compat5.mlp b/grammar/compat5.mlp
deleted file mode 100644
index 8473a1fb7..000000000
--- a/grammar/compat5.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
-    - GEXTEND ... becomes EXTEND ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
-  | [< '(KEYWORD "GEXTEND", loc); s >] ->
-    [< '(KEYWORD "EXTEND", loc); my_token_filter s >]
-  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
-  | [< >] -> [< >]
-
-let _ =
-  Token.Filter.define_filter (Gram.get_filter())
-    (fun prev strm -> prev (my_token_filter strm))
diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp
deleted file mode 100644
index 46802a825..000000000
--- a/grammar/compat5b.mlp
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Adding a bit of camlp5 syntax to camlp4 for compatibility:
-    - EXTEND ... becomes EXTEND Gram ...
-*)
-
-open Camlp4.PreCast
-
-let rec my_token_filter = parser
-  | [< '(KEYWORD "EXTEND",_ as t); s >] ->
-    [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >]
-  | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >]
-  | [< >] -> [< >]
-
-let _ =
-  Token.Filter.define_filter (Gram.get_filter())
-    (fun prev strm -> prev (my_token_filter strm))
diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp
deleted file mode 100644
index 6246da7bb..000000000
--- a/grammar/gramCompat.mlp
+++ /dev/null
@@ -1,86 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file depending on ocaml/camlp4 version *)
-
-(** Misc module emulation *)
-
-IFDEF CAMLP5 THEN
-
-module CompatLoc = struct
-  include Ploc
-  let ghost = dummy
-  let merge = encl
-end
-
-ELSE
-
-module CompatLoc = Camlp4.PreCast.Loc
-
-END
-
-IFDEF CAMLP5 THEN
-
-module PcamlSig = struct end
-
-ELSE
-
-module PcamlSig = Camlp4.Sig
-module Ast = Camlp4.PreCast.Ast
-module Pcaml = Camlp4.PreCast.Syntax
-module MLast = Ast
-
-END
-
-(** Compatibility with camlp5 strict mode *)
-IFDEF CAMLP5 THEN
-  IFDEF STRICT THEN
-    let vala x = Ploc.VaVal x
-  ELSE
-    let vala x = x
-  END
-ELSE
-  let vala x = x
-END
-
-(** Fix a quotation difference in [str_item] *)
-
-let declare_str_items loc l =
-IFDEF CAMLP5 THEN
-  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
-ELSE
-  Ast.stSem_of_list l
-END
-
-(** Quotation difference for match clauses *)
-
-let default_patt loc =
-  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
-
-IFDEF CAMLP5 THEN
-
-let make_fun loc cl =
-  let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
-
-ELSE
-
-let make_fun loc cl =
-  let mk_when = function
-    | Some w -> w
-    | None -> Ast.ExNil loc
-  in
-  let mk_clause (patt,optwhen,expr) =
-    (* correspond to <:match_case< ... when ... -> ... >> *)
-    Ast.McArr (loc, patt, mk_when optwhen, expr) in
-  let init = mk_clause (default_patt loc) in
-  let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in
-  let l = List.fold_right add_clause cl init in
-  Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *)
-
-END
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 37ec1d56a..5b3eb3202 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open GramCompat (* necessary for camlp4 *)
-
 type argument_type =
 | ListArgType of argument_type
 | OptArgType of argument_type
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 0dd096ef7..8b930cf36 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -8,8 +8,6 @@
 
 (* This file defines standard combinators to build ml expressions *)
 
-open GramCompat
-
 type argument_type =
 | ListArgType of argument_type
 | OptArgType of argument_type
@@ -33,17 +31,17 @@ let mlexpr_of_list f l =
   List.fold_right
     (fun e1 e2 ->
       let e1 = f e1 in
-       let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+       let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
        <:expr< [$e1$ :: $e2$] >>)
-    l (let loc = CompatLoc.ghost in <:expr< [] >>)
+    l (let loc = Ploc.dummy in <:expr< [] >>)
 
 let mlexpr_of_pair m1 m2 (a1,a2) =
   let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
+  let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
   <:expr< ($e1$, $e2$) >>
 
 (* We don't give location for tactic quotation! *)
-let loc = CompatLoc.ghost
+let loc = Ploc.dummy
 
 
 let mlexpr_of_bool = function
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 8c0614a7b..f57be9022 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -10,7 +10,15 @@
 
 open Q_util
 open Argextend
-open GramCompat
+
+(** Quotation difference for match clauses *)
+
+let default_patt loc =
+  (<:patt< _ >>, Ploc.VaVal None, <:expr< failwith "Extension: cannot occur" >>)
+
+let make_fun loc cl =
+  let l = cl @ [default_patt loc] in
+  MLast.ExFun (loc, Ploc.VaVal l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
 
 let dloc = <:expr< Loc.ghost >>
 
@@ -41,11 +49,11 @@ let rec make_let raw e = function
 
 let make_clause (pt,_,e) =
   (make_patt pt,
-   vala None,
+   Ploc.VaVal None,
    make_let false e pt)
 
 let make_fun_clauses loc s l =
-  let map c = GramCompat.make_fun loc [make_clause c] in
+  let map c = make_fun loc [make_clause c] in
   mlexpr_of_list map l
 
 let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >>
@@ -100,7 +108,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
         whole-prof tactics like [shelve_unifiable]. *)
       <:expr< fun _ $lid:"ist"$ -> $tac$ >>
   | _ ->
-      let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+      let f = make_fun loc [patt, Ploc.VaVal None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
       <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
   in
   (** Arguments are not passed directly to the ML tactic in the TacML node,
@@ -129,7 +137,6 @@ let declare_tactic loc tacname ~level classification clause = match clause with
     ]
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 04b117fba..d4857b1df 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -11,7 +11,6 @@
 open Q_util
 open Argextend
 open Tacextend
-open GramCompat
 
 type rule = {
   r_head : string option;
@@ -37,7 +36,7 @@ let rec make_let e = function
 
 let make_clause { r_patt = pt; r_branch = e; } =
   (make_patt pt,
-   vala None,
+   Ploc.VaVal None,
    make_let e pt)
 
 (* To avoid warnings *)
@@ -55,11 +54,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
   match c ,cg with
   | Some c, _ ->
      (make_patt pt,
-      vala None,
+      Ploc.VaVal None,
       make_let (mk_ignore c pt) pt)
   | None, Some cg ->
      (make_patt pt,
-      vala None,
+      Ploc.VaVal None,
       <:expr< fun () -> $cg$ $str:s$ >>)
   | None, None -> prerr_endline
       (("Vernac entry \""^s^"\" misses a classifier. "^
@@ -82,7 +81,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
        ("Specific classifiers have precedence over global "^
          "classifiers. Only one classifier is called.") ^ "\n");
     (make_patt pt,
-      vala None,
+      Ploc.VaVal None,
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
 
 let make_fun_clauses loc s l =
@@ -91,13 +90,13 @@ let make_fun_clauses loc s l =
     | None -> false
     | Some () -> true
     in
-    let cl = GramCompat.make_fun loc [make_clause c] in
+    let cl = make_fun loc [make_clause c] in
     <:expr< ($mlexpr_of_bool depr$, $cl$)>>
   in
   mlexpr_of_list map l
 
 let make_fun_classifiers loc s c l =
-  let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in
+  let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in
   mlexpr_of_list (fun x -> x) cl
 
 let make_prod_item = function
@@ -128,7 +127,6 @@ let declare_command loc s c nt cl =
       } >> ]
 
 open Pcaml
-open PcamlSig (* necessary for camlp4 *)
 
 EXTEND
   GLOBAL: str_item;