[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.

4 files changed, 23 insertions, 27 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 368b23be3..cf2e42d2c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 open Ltac_plugin
-open Compat
 open Util
 open Term
 open Pp
@@ -17,6 +16,7 @@ open Indfun
 open Genarg
 open Stdarg
 open Misctypes
+open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index fd33a779d..ece0adb07 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -12,7 +12,6 @@ DECLARE PLUGIN "ltac_plugin"
 
 open Util
 open Pp
-open Compat
 open Constrexpr
 open Tacexpr
 open Misctypes
@@ -68,9 +67,9 @@ let _ =
 let test_bracket_ident =
   Gram.Entry.of_parser "test_bracket_ident"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
         | KEYWORD "[" ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | IDENT _ -> ()
 	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index fa01baab7..4b3ca80af 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -14,7 +14,6 @@ open Genredexpr
 open Constrexpr
 open Libnames
 open Tok
-open Compat
 open Misctypes
 open Locus
 open Decl_kinds
@@ -34,11 +33,11 @@ let err () = raise Stream.Failure
 let test_lpar_id_coloneq =
   Gram.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
         | KEYWORD "(" ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | IDENT _ ->
-                  (match get_tok (stream_nth 2 strm) with
+                  (match stream_nth 2 strm with
 	            | KEYWORD ":=" -> ()
 	            | _ -> err ())
 	      | _ -> err ())
@@ -48,11 +47,11 @@ let test_lpar_id_coloneq =
 let test_lpar_id_rpar =
   Gram.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
         | KEYWORD "(" ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | IDENT _ ->
-                  (match get_tok (stream_nth 2 strm) with
+                  (match stream_nth 2 strm with
 	            | KEYWORD ")" -> ()
 	            | _ -> err ())
 	      | _ -> err ())
@@ -62,11 +61,11 @@ let test_lpar_id_rpar =
 let test_lpar_idnum_coloneq =
   Gram.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
         | KEYWORD "(" ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | IDENT _ | INT _ ->
-                  (match get_tok (stream_nth 2 strm) with
+                  (match stream_nth 2 strm with
                     | KEYWORD ":=" -> ()
                     | _ -> err ())
               | _ -> err ())
@@ -76,11 +75,11 @@ let test_lpar_idnum_coloneq =
 let test_lpar_id_colon =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
         | KEYWORD "(" ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | IDENT _ ->
-                  (match get_tok (stream_nth 2 strm) with
+                  (match stream_nth 2 strm with
                     | KEYWORD ":" -> ()
                     | _ -> err ())
               | _ -> err ())
@@ -91,30 +90,30 @@ let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       let rec skip_to_rpar p n =
-	match get_tok (List.last (Stream.npeek n strm)) with
+	match List.last (Stream.npeek n strm) with
         | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
         | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1)
 	| KEYWORD "." -> err ()
 	| _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
-	match get_tok (List.last (Stream.npeek n strm)) with
+	match List.last (Stream.npeek n strm) with
         | IDENT _ | KEYWORD "_" -> skip_names (n+1)
 	| KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
 	| _ -> err () in
       let rec skip_binders n =
-	match get_tok (List.last (Stream.npeek n strm)) with
+	match List.last (Stream.npeek n strm) with
         | KEYWORD "(" -> skip_binders (skip_names (n+1))
         | IDENT _ | KEYWORD "_" -> skip_binders (n+1)
 	| KEYWORD ":=" -> ()
 	| _ -> err () in
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
       | KEYWORD "(" -> skip_binders 2
       | _ -> err ())
 
 let lookup_at_as_comma =
   Gram.Entry.of_parser "lookup_at_as_comma"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
 	| KEYWORD (","|"at"|"as") -> ()
 	| _ -> err ())
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 4d5594633..3d0232d94 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -10,7 +10,7 @@
 
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
  * we thus save the lexer to restore it at the end of the file *)
-let frozen_lexer = CLexer.freeze () ;;
+let frozen_lexer = CLexer.get_keyword_state () ;;
 
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
@@ -1040,7 +1040,7 @@ let interp_open_constr ist gl gc =
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
 let interp_term ist gl (_, c) = (interp_open_constr ist gl c)
 let pr_ssrterm _ _ _ = pr_term
-let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
+let input_ssrtermkind strm = match stream_nth 0 strm with
   | Tok.KEYWORD "(" -> '('
   | Tok.KEYWORD "@" -> '@'
   | _ -> ' '
@@ -1057,8 +1057,6 @@ ARGUMENT EXTEND cpattern
 | [ "Qed" constr(c) ] -> [ mk_lterm c ]
 END
 
-let (!@) = Compat.to_coqloc
-
 GEXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr ->
@@ -1444,6 +1442,6 @@ END
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
 (* consequence the extended ssreflect grammar.                             *)
-let () = CLexer.unfreeze frozen_lexer ;;
+let () = CLexer.set_keyword_state frozen_lexer ;;
 
 (* vim: set filetype=ocaml foldmethod=marker: *)