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

10 files changed, 380 insertions, 520 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 3b84eaa81..6d259e1b1 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -9,7 +9,17 @@
 open Pp
 open Util
 open Tok
-open Compat
+
+let to_coqloc loc =
+  { Loc.fname = Ploc.file_name loc;
+    Loc.line_nb = Ploc.line_nb loc;
+    Loc.bol_pos = Ploc.bol_pos loc;
+    Loc.bp = Ploc.first_pos loc;
+    Loc.ep = Ploc.last_pos loc;
+    Loc.line_nb_last = Ploc.line_nb_last loc;
+    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
+
+let (!@) = to_coqloc
 
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
@@ -110,11 +120,52 @@ module Error = struct
 end
 open Error
 
-let err loc str = Loc.raise ~loc:(Compat.to_coqloc loc) (Error.E str)
+let err loc str = Loc.raise ~loc:(to_coqloc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
-(* Lexer conventions on tokens *)
+(** Location utilities  *)
+let file_loc_of_file = function
+| None -> ""
+| Some f -> f
+
+let make_loc fname line_nb bol_pos bp ep =
+  Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
+
+(* Update a loc without allocating an intermediate pair *)
+let set_loc_pos loc bp ep =
+  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
+
+(* Increase line number by 1 and update position of beginning of line *)
+let bump_loc_line loc bol_pos =
+  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
+		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+
+(* Same as [bump_loc_line], but for the last line in location *)
+(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
+   so we have to resort to a hack merging two locations. *)
+(* Warning: [bump_loc_line_last] changes the end position. You may need to call
+   [set_loc_pos] to fix it. *)
+let bump_loc_line_last loc bol_pos =
+  let loc' =
+    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
+		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
+  in
+  Ploc.encl loc loc'
+
+let set_loc_file loc fname =
+  Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc)
+		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+
+(* For some reason, the [Ploc.after] function of Camlp5 does not update line
+   numbers, so we define our own function that does it. *)
+let after loc =
+  let line_nb = Ploc.line_nb_last loc in
+  let bol_pos = Ploc.bol_pos_last loc in
+  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
+		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
+
+(** Lexer conventions on tokens *)
 
 type token_kind =
   | Utf8Token of (Unicode.status * int)
@@ -186,7 +237,7 @@ let check_keyword str =
   let rec loop_symb = parser
     | [< ' (' ' | '\n' | '\r' | '\t' | '"') >] -> bad_token str
     | [< s >] ->
-        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
+        match unlocated lookup_utf8 Ploc.dummy s with
         | Utf8Token (_,n) -> njunk n s; loop_symb s
         | AsciiChar -> Stream.junk s; loop_symb s
         | EmptyStream -> ()
@@ -200,7 +251,7 @@ let check_ident str =
     | [< ' ('0'..'9' | ''') when intail; s >] ->
         loop_id true s
     | [< s >] ->
-        match unlocated lookup_utf8 Compat.CompatLoc.ghost s with
+        match unlocated lookup_utf8 Ploc.dummy s with
         | Utf8Token (Unicode.Letter, n) -> njunk n s; loop_id true s
         | Utf8Token (Unicode.IdentPart, n) when intail ->
           njunk n s;
@@ -233,10 +284,10 @@ let remove_keyword str =
 let keywords () = ttree_elements !token_tree
 
 (* Freeze and unfreeze the state of the lexer *)
-type frozen_t = ttree
+type keyword_state = ttree
 
-let freeze () = !token_tree
-let unfreeze tt = (token_tree := tt)
+let get_keyword_state () = !token_tree
+let set_keyword_state tt = (token_tree := tt)
 
 (* The string buffering machinery *)
 
@@ -621,8 +672,6 @@ let loct_add loct i loc = Hashtbl.add loct i loc
    we unfreeze the state of the lexer. This restores the behaviour of the
    lexer. B.B. *)
 
-IFDEF CAMLP5 THEN
-
 type te = Tok.t
 
 (** Names of tokens, for this lexer, used in Grammar error messages *)
@@ -640,12 +689,12 @@ let token_text = function
 
 let func cs =
   let loct = loct_create () in
-  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
+  let cur_loc = ref (make_loc !current_file 1 0 0 0) in
   let ts =
     Stream.from
       (fun i ->
          let (tok, loc) = next_token !cur_loc cs in
-	 cur_loc := Compat.after loc;
+	 cur_loc := after loc;
          loct_add loct i loc; Some tok)
   in
   (ts, loct_func loct)
@@ -661,41 +710,6 @@ let lexer = {
   Token.tok_comm = None;
   Token.tok_text = token_text }
 
-ELSE (* official camlp4 for ocaml >= 3.10 *)
-
-module M_ = Camlp4.ErrorHandler.Register (Error)
-
-module Loc = Compat.CompatLoc
-module Token = struct
-  include Tok (* Cf. tok.ml *)
-  module Loc = Compat.CompatLoc
-  module Error = Camlp4.Struct.EmptyError
-  module Filter = struct
-    type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
-    type t = unit
-    let mk _is_kwd = ()
-    let keyword_added () kwd _ = add_keyword kwd
-    let keyword_removed () _ = ()
-    let filter () x = x
-    let define_filter () _ = ()
-  end
-end
-
-let mk () =
-  let loct = loct_create () in
-  let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in
-  let rec self init_loc (* FIXME *) =
-    parser i
-       [< (tok, loc) = next_token !cur_loc; s >] ->
-            cur_loc := Compat.set_loc_file loc !current_file;
-	    loct_add loct i loc;
-            [< '(tok, loc); self init_loc s >]
-      | [< >] -> [< >]
-  in
-  self
-
-END
-
 (** Terminal symbols interpretation *)
 
 let is_ident_not_keyword s =
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index e0fdf8cb5..1a1c302f2 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -6,27 +6,57 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** This should be functional but it is not due to the interface *)
 val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 val keywords : unit -> CString.Set.t
 
+type keyword_state
+val set_keyword_state : keyword_state -> unit
+val get_keyword_state : unit -> keyword_state
+
 val check_ident : string -> unit
 val is_ident : string -> bool
 val check_keyword : string -> unit
 
-type frozen_t
-val freeze : unit -> frozen_t
-val unfreeze : frozen_t -> unit
-
 val xml_output_comment : (string -> unit) Hook.t
 
-(* Retrieve the comments lexed at a given location of the stream
-   currently being processeed *)
-val extract_comments : int -> string list
-
 val terminal : string -> Tok.t
 
 (** The lexer of Coq: *)
 
-include Compat.LexerSig
+(* modtype Grammar.GLexerType: sig
+     type te val
+     lexer : te Plexing.lexer
+   end
+
+where
+
+  type lexer 'te =
+    { tok_func : lexer_func 'te;
+      tok_using : pattern -> unit;
+      tok_removing : pattern -> unit;
+      tok_match : pattern -> 'te -> string;
+      tok_text : pattern -> string;
+      tok_comm : mutable option (list location) }
+ *)
+include Grammar.GLexerType with type te = Tok.t
+
+module Error : sig
+  type t
+  exception E of t
+  val to_string : t -> string
+end
+
+(* Mainly for comments state, etc... *)
+type lexer_state
+
+val init_lexer_state : string option -> lexer_state
+val set_lexer_state : lexer_state -> unit
+val release_lexer_state : unit -> lexer_state
+val drop_lexer_state : unit -> unit
+
+(* Retrieve the comments lexed at a given location of the stream
+   currently being processeed *)
+val extract_comments : int -> string list
diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
deleted file mode 100644
index 4a36af2d8..000000000
--- a/parsing/compat.ml4
+++ /dev/null
@@ -1,421 +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 *)
-
-(** Locations *)
-
-let file_loc_of_file = function
-| None -> ""
-| Some f -> f
-
-IFDEF CAMLP5 THEN
-
-module CompatLoc = struct
-  include Ploc
-  let ghost = dummy
-  let merge = encl
-end
-
-exception Exc_located = Ploc.Exc
-
-let to_coqloc loc =
-  { Loc.fname = Ploc.file_name loc;
-    Loc.line_nb = Ploc.line_nb loc;
-    Loc.bol_pos = Ploc.bol_pos loc;
-    Loc.bp = Ploc.first_pos loc;
-    Loc.ep = Ploc.last_pos loc;
-    Loc.line_nb_last = Ploc.line_nb_last loc;
-    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
-
-let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) ""
-
-(* Update a loc without allocating an intermediate pair *)
-let set_loc_pos loc bp ep =
-  Ploc.sub loc (bp - Ploc.first_pos loc) (ep - bp)
-
-(* Increase line number by 1 and update position of beginning of line *)
-let bump_loc_line loc bol_pos =
-  Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb loc + 1) bol_pos
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
-(* Same as [bump_loc_line], but for the last line in location *)
-(* For an obscure reason, camlp5 does not give an easy way to set line_nb_stop,
-   so we have to resort to a hack merging two locations. *)
-(* Warning: [bump_loc_line_last] changes the end position. You may need to call
-   [set_loc_pos] to fix it. *)
-let bump_loc_line_last loc bol_pos =
-  let loc' =
-    Ploc.make_loc (Ploc.file_name loc) (Ploc.line_nb_last loc + 1) bol_pos
-		  (Ploc.first_pos loc + 1, Ploc.last_pos loc + 1) (Ploc.comment loc)
-  in
-  Ploc.encl loc loc'
-
-let set_loc_file loc fname =
-  Ploc.make_loc fname (Ploc.line_nb loc) (Ploc.bol_pos loc)
-		(Ploc.first_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
-(* For some reason, the [Ploc.after] function of Camlp5 does not update line
-   numbers, so we define our own function that does it. *)
-let after loc =
-  let line_nb = Ploc.line_nb_last loc in
-  let bol_pos = Ploc.bol_pos_last loc in
-  Ploc.make_loc (Ploc.file_name loc) line_nb bol_pos
-		(Ploc.last_pos loc, Ploc.last_pos loc) (Ploc.comment loc)
-
-ELSE
-
-module CompatLoc = Camlp4.PreCast.Loc
-
-exception Exc_located = CompatLoc.Exc_located
-
-let to_coqloc loc =
-  { Loc.fname = CompatLoc.file_name loc;
-    Loc.line_nb = CompatLoc.start_line loc;
-    Loc.bol_pos = CompatLoc.start_bol loc;
-    Loc.bp = CompatLoc.start_off loc;
-    Loc.ep = CompatLoc.stop_off loc;
-    Loc.line_nb_last = CompatLoc.stop_line loc;
-    Loc.bol_pos_last = CompatLoc.stop_bol loc; }
-
-let make_loc fname line_nb bol_pos start stop =
-  CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false)
-
-open CompatLoc
-
-let set_loc_pos loc bp ep =
-  of_tuple (file_name loc, start_line loc, start_bol loc, bp,
-	    stop_line loc, stop_bol loc, ep, is_ghost loc)
-
-let bump_loc_line loc bol_pos =
-  of_tuple (file_name loc, start_line loc + 1, bol_pos, start_off loc,
-	    start_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
-
-let bump_loc_line_last loc bol_pos =
-  of_tuple (file_name loc, start_line loc, start_bol loc, start_off loc,
-	    stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc)
-
-let set_loc_file loc fname =
-  of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc,
-	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
-
-let after loc =
-  of_tuple (file_name loc, stop_line loc, stop_bol loc, stop_off loc,
-	    stop_line loc, stop_bol loc, stop_off loc, is_ghost loc)
-
-END
-
-let (!@) = to_coqloc
-
-(** Misc module emulation *)
-
-IFDEF CAMLP5 THEN
-
-module PcamlSig = struct end
-module Token = Token
-module CompatGramext = struct include Gramext type assoc = g_assoc end
-
-ELSE
-
-module PcamlSig = Camlp4.Sig
-module Ast = Camlp4.PreCast.Ast
-module Pcaml = Camlp4.PreCast.Syntax
-module MLast = Ast
-module Token = struct exception Error of string end
-module CompatGramext = Camlp4.Sig.Grammar
-
-END
-
-(** Signature of CLexer *)
-
-IFDEF CAMLP5 THEN
-
-module type LexerSig = sig
-  include Grammar.GLexerType with type te = Tok.t
-  module Error : sig
-    type t
-    exception E of t
-    val to_string : t -> string
-  end
-  type lexer_state
-  val init_lexer_state : string option -> lexer_state
-  val set_lexer_state : lexer_state -> unit
-  val release_lexer_state : unit -> lexer_state
-  val drop_lexer_state : unit -> unit
-end
-
-ELSE
-
-module type LexerSig = sig
-  include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
-  type lexer_state
-  val init_lexer_state : string option -> lexer_state
-  val set_lexer_state : lexer_state -> unit
-  val release_lexer_state : unit -> lexer_state
-  val drop_lexer_state : unit -> unit
-end
-
-END
-
-(** Signature and implementation of grammars *)
-
-IFDEF CAMLP5 THEN
-
-module type GrammarSig = sig
-  include Grammar.S with type te = Tok.t
-  type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statment =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
-  type coq_parsable
-  val parsable : ?file:string -> char Stream.t -> coq_parsable
-  val action : 'a -> action
-  val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
-  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
-  val srules' : production_rule list -> symbol
-  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-end
-
-module GrammarMake (L:LexerSig) : GrammarSig = struct
-  include Grammar.GMake (L)
-  type 'a entry = 'a Entry.e
-  type internal_entry = Tok.t Gramext.g_entry
-  type symbol = Tok.t Gramext.g_symbol
-  type action = Gramext.g_action
-  type production_rule = symbol list * action
-  type single_extend_statment =
-      string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
-  type coq_parsable = parsable * L.lexer_state ref
-  let parsable ?file c =
-    let state = ref (L.init_lexer_state file) in
-    L.set_lexer_state !state;
-    let a = parsable c in
-    state := L.release_lexer_state ();
-    (a,state)
-  let action = Gramext.action
-  let entry_create = Entry.create
-  let entry_parse e (p,state) =
-    L.set_lexer_state !state;
-    try
-      let c = Entry.parse e p in
-      state := L.release_lexer_state ();
-      c
-    with Exc_located (loc,e) ->
-      L.drop_lexer_state ();
-      let loc' = Loc.get_loc (Exninfo.info e) in
-      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
-      Loc.raise ~loc e
-  let with_parsable (p,state) f x =
-    L.set_lexer_state !state;
-    try
-      let a = f x in
-      state := L.release_lexer_state ();
-      a
-    with e ->
-      L.drop_lexer_state ();
-      raise e
-
-  let entry_print ft x = Entry.print ft x
-  let srules' = Gramext.srules
-  let parse_tokens_after_filter = Entry.parse_token
-end
-
-ELSE
-
-module type GrammarSig = sig
-  include Camlp4.Sig.Grammar.Static
-    with module Loc = CompatLoc and type Token.t = Tok.t
-  type 'a entry = 'a Entry.t
-  type action = Action.t
-  type coq_parsable
-  val parsable : ?file:string -> char Stream.t -> coq_parsable
-  val action : 'a -> action
-  val entry_create : string -> 'a entry
-  val entry_parse : 'a entry -> coq_parsable -> 'a
-  val entry_print : Format.formatter -> 'a entry -> unit
-  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
-  val srules' : production_rule list -> symbol
-end
-
-module GrammarMake (L:LexerSig) : GrammarSig = struct
-  (* We need to refer to Coq's module Loc before it is hidden by include *)
-  let raise_coq_loc loc e = Loc.raise ~loc:(to_coqloc loc) e
-  include Camlp4.Struct.Grammar.Static.Make (L)
-  type 'a entry = 'a Entry.t
-  type action = Action.t
-  type coq_parsable = char Stream.t * L.lexer_state ref
-  let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state)
-  let action = Action.mk
-  let entry_create = Entry.mk
-  let entry_parse e (s,state) =
-    L.set_lexer_state !state;
-    try
-      let c = parse e (*FIXME*)CompatLoc.ghost s in
-      state := L.release_lexer_state ();
-      c
-    with Exc_located (loc,e) ->
-      L.drop_lexer_state ();
-      raise_coq_loc loc e;;
-  let with_parsable (p,state) f x =
-    L.set_lexer_state !state;
-    try
-      let a = f x in
-      state := L.release_lexer_state ();
-      a
-    with e ->
-      L.drop_lexer_state ();
-      Pervasives.raise e;;
-  let entry_print ft x = Entry.print ft x
-  let srules' = srules (entry_create "dummy")
-end
-
-END
-
-(** Some definitions are grammar-specific in Camlp4, so we use a functor to
-    depend on it while taking a dummy argument in Camlp5. *)
-
-module GramextMake (G : GrammarSig) :
-sig
-  val stoken : Tok.t -> G.symbol
-  val sself : G.symbol
-  val snext : G.symbol
-  val slist0 : G.symbol -> G.symbol
-  val slist0sep : G.symbol * G.symbol -> G.symbol
-  val slist1 : G.symbol -> G.symbol
-  val slist1sep : G.symbol * G.symbol -> G.symbol
-  val sopt : G.symbol -> G.symbol
-  val snterml : G.internal_entry * string -> G.symbol
-  val snterm : G.internal_entry -> G.symbol
-  val snterml_level : G.symbol -> string
-end =
-struct
-
-IFDEF CAMLP5 THEN
-  let stoken tok =
-    let pattern = match tok with
-    | Tok.KEYWORD s -> "", s
-    | Tok.IDENT s -> "IDENT", s
-    | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
-    | Tok.FIELD s -> "FIELD", s
-    | Tok.INT s -> "INT", s
-    | Tok.STRING s -> "STRING", s
-    | Tok.LEFTQMARK -> "LEFTQMARK", ""
-    | Tok.BULLET s -> "BULLET", s
-    | Tok.EOI -> "EOI", ""
-    in
-    Gramext.Stoken pattern
-ELSE
-  module Gramext = G
-  let stoken tok = match tok with
-  | Tok.KEYWORD s -> Gramext.Skeyword s
-  | tok -> Gramext.Stoken (Tok.equal tok, G.Token.to_string tok)
-END
-
-  IFDEF CAMLP5 THEN
-     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
-     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
-  ELSE
-    let slist0sep (x, y) = Gramext.Slist0sep (x, y)
-    let slist1sep (x, y) = Gramext.Slist1sep (x, y)
-  END
-
-  let snterml (x, y) = Gramext.Snterml (x, y)
-  let snterm x = Gramext.Snterm x
-  let sself = Gramext.Sself
-  let snext = Gramext.Snext
-  let slist0 x = Gramext.Slist0 x
-  let slist1 x = Gramext.Slist1 x
-  let sopt x = Gramext.Sopt x
-
-  let snterml_level = function
-  | Gramext.Snterml (_, l) -> l
-  | _ -> failwith "snterml_level"
-
-end
-
-
-(** Misc functional adjustments *)
-
-(** - The lexer produces streams made of pairs in camlp4 *)
-
-let get_tok = IFDEF CAMLP5 THEN fun x -> x ELSE fst END
-
-(** - Gram.extend is more currified in camlp5 than in camlp4 *)
-
-IFDEF CAMLP5 THEN
-let maybe_curry f x y = f (x,y)
-let maybe_uncurry f (x,y) = f x y
-ELSE
-let maybe_curry f = f
-let maybe_uncurry f = f
-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
-
-IFDEF CAMLP5 THEN
-let warning_verbose = Gramext.warning_verbose
-ELSE
-(* TODO: this is a workaround, since there isn't such
-   [warning_verbose] in new camlp4. *)
-let warning_verbose = ref true
-END
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index c127e7880..05cb74ddc 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -12,7 +12,6 @@ open Constrexpr
 open Constrexpr_ops
 open Util
 open Tok
-open Compat
 open Misctypes
 open Decl_kinds
 
@@ -81,11 +80,11 @@ let err () = raise Stream.Failure
 let lpar_id_coloneq =
   Gram.Entry.of_parser "test_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 s ->
-                  (match get_tok (stream_nth 2 strm) with
+                  (match stream_nth 2 strm with
                     | KEYWORD ":=" ->
                         stream_njunk 3 strm;
                         Names.Id.of_string s
@@ -96,9 +95,9 @@ let lpar_id_coloneq =
 let impl_ident_head =
   Gram.Entry.of_parser "impl_ident_head"
     (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 ("wf"|"struct"|"measure") -> err ()
 	      | IDENT s ->
 		  stream_njunk 2 strm;
@@ -109,15 +108,15 @@ let impl_ident_head =
 let name_colon =
   Gram.Entry.of_parser "name_colon"
     (fun strm ->
-      match get_tok (stream_nth 0 strm) with
+      match stream_nth 0 strm with
 	| IDENT s ->
-            (match get_tok (stream_nth 1 strm) with
+            (match stream_nth 1 strm with
               | KEYWORD ":" ->
                   stream_njunk 2 strm;
                   Name (Names.Id.of_string s)
               | _ -> err ())
 	| KEYWORD "_" ->
-          (match get_tok (stream_nth 1 strm) with
+          (match stream_nth 1 strm with
               | KEYWORD ":" ->
                   stream_njunk 2 strm;
                   Anonymous
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2db91b8f8..2af4ed533 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Names
 open Libnames
 open Tok (* necessary for camlp4 *)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 4c5280538..7ca2e4a4f 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Compat
 open Constrexpr
 open Vernacexpr
 open Misctypes
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ded7a557c..71b93439b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Compat
 open CErrors
 open Util
 open Names
@@ -407,7 +406,7 @@ let only_starredidentrefs =
   Gram.Entry.of_parser "test_only_starredidentrefs"
     (fun strm ->
       let rec aux n =
-      match get_tok (Util.stream_nth n strm) with
+      match Util.stream_nth n strm with
         | KEYWORD "." -> ()
         | KEYWORD ")" -> ()
         | (IDENT _ | KEYWORD "Type" | KEYWORD "*") -> aux (n+1)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 0e1c79c91..2a73d7bc6 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,5 +1,4 @@
 Tok
-Compat
 CLexer
 Pcoq
 Egramml
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b8405ca8c..92d249e53 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -7,31 +7,203 @@
 (************************************************************************)
 
 open Pp
-open Compat
 open CErrors
 open Util
 open Extend
 open Genarg
 
+let curry f x y = f (x, y)
+let uncurry f (x,y) = f x y
+
+(** Location Utils  *)
+let to_coqloc loc =
+  { Loc.fname = Ploc.file_name loc;
+    Loc.line_nb = Ploc.line_nb loc;
+    Loc.bol_pos = Ploc.bol_pos loc;
+    Loc.bp = Ploc.first_pos loc;
+    Loc.ep = Ploc.last_pos loc;
+    Loc.line_nb_last = Ploc.line_nb_last loc;
+    Loc.bol_pos_last = Ploc.bol_pos_last loc; }
+
+let (!@) = to_coqloc
+
 (** The parser of Coq *)
+module G : sig
+
+  include Grammar.S with type te = Tok.t
+
+(* where Grammar.S
+
+module type S =
+  sig
+    type te = 'x;
+    type parsable = 'x;
+    value parsable : Stream.t char -> parsable;
+    value tokens : string -> list (string * int);
+    value glexer : Plexing.lexer te;
+    value set_algorithm : parse_algorithm -> unit;
+    module Entry :
+      sig
+        type e 'a = 'y;
+        value create : string -> e 'a;
+        value parse : e 'a -> parsable -> 'a;
+        value parse_token : e 'a -> Stream.t te -> 'a;
+        value name : e 'a -> string;
+        value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
+        value print : Format.formatter -> e 'a -> unit;
+        external obj : e 'a -> Gramext.g_entry te = "%identity";
+      end
+    ;
+    module Unsafe :
+      sig
+        value gram_reinit : Plexing.lexer te -> unit;
+        value clear_entry : Entry.e 'a -> unit;
+      end
+    ;
+    value extend :
+      Entry.e 'a -> option Gramext.position ->
+        list
+          (option string * option Gramext.g_assoc *
+           list (list (Gramext.g_symbol te) * Gramext.g_action)) ->
+        unit;
+    value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit;
+  end
+  *)
+
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * Gramext.g_assoc option * production_rule list
+  type extend_statment =
+      Gramext.position option * single_extend_statment list
+  type coq_parsable
+
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> coq_parsable -> 'a
+  val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
+  val srules' : production_rule list -> symbol
+  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
+
+end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
+
+  include Grammar.GMake(CLexer)
+
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * Gramext.g_assoc option * production_rule list
+  type extend_statment =
+      Gramext.position option * single_extend_statment list
+  type coq_parsable = parsable * CLexer.lexer_state ref
+
+  let parsable ?file c =
+    let state = ref (CLexer.init_lexer_state file) in
+    CLexer.set_lexer_state !state;
+    let a = parsable c in
+    state := CLexer.release_lexer_state ();
+    (a,state)
+
+  let action = Gramext.action
+  let entry_create = Entry.create
+
+  let entry_parse e (p,state) =
+    CLexer.set_lexer_state !state;
+    try
+      let c = Entry.parse e p in
+      state := CLexer.release_lexer_state ();
+      c
+    with Ploc.Exc (loc,e) ->
+      CLexer.drop_lexer_state ();
+      let loc' = Loc.get_loc (Exninfo.info e) in
+      let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in
+      Loc.raise ~loc e
+
+  let with_parsable (p,state) f x =
+    CLexer.set_lexer_state !state;
+    try
+      let a = f x in
+      state := CLexer.release_lexer_state ();
+      a
+    with e ->
+      CLexer.drop_lexer_state ();
+      raise e
+
+  let entry_print ft x = Entry.print ft x
+
+  (* Not used *)
+  let srules' = Gramext.srules
+  let parse_tokens_after_filter = Entry.parse_token
+
+end
 
-module G = GrammarMake (CLexer)
 
-let warning_verbose = Compat.warning_verbose
+let warning_verbose = Gramext.warning_verbose
 
 let of_coq_assoc = function
-| Extend.RightA -> CompatGramext.RightA
-| Extend.LeftA -> CompatGramext.LeftA
-| Extend.NonA -> CompatGramext.NonA
+| Extend.RightA -> Gramext.RightA
+| Extend.LeftA -> Gramext.LeftA
+| Extend.NonA -> Gramext.NonA
 
 let of_coq_position = function
-| Extend.First -> CompatGramext.First
-| Extend.Last -> CompatGramext.Last
-| Extend.Before s -> CompatGramext.Before s
-| Extend.After s -> CompatGramext.After s
-| Extend.Level s -> CompatGramext.Level s
+| Extend.First -> Gramext.First
+| Extend.Last -> Gramext.Last
+| Extend.Before s -> Gramext.Before s
+| Extend.After s -> Gramext.After s
+| Extend.Level s -> Gramext.Level s
+
+module Symbols : sig
+  val stoken : Tok.t -> G.symbol
+  val sself : G.symbol
+  val snext : G.symbol
+  val slist0 : G.symbol -> G.symbol
+  val slist0sep : G.symbol * G.symbol -> G.symbol
+  val slist1 : G.symbol -> G.symbol
+  val slist1sep : G.symbol * G.symbol -> G.symbol
+  val sopt : G.symbol -> G.symbol
+  val snterml : G.internal_entry * string -> G.symbol
+  val snterm : G.internal_entry -> G.symbol
+  val snterml_level : G.symbol -> string
+end = struct
+
+  let stoken tok =
+    let pattern = match tok with
+    | Tok.KEYWORD s -> "", s
+    | Tok.IDENT s -> "IDENT", s
+    | Tok.PATTERNIDENT s -> "PATTERNIDENT", s
+    | Tok.FIELD s -> "FIELD", s
+    | Tok.INT s -> "INT", s
+    | Tok.STRING s -> "STRING", s
+    | Tok.LEFTQMARK -> "LEFTQMARK", ""
+    | Tok.BULLET s -> "BULLET", s
+    | Tok.EOI -> "EOI", ""
+    in
+    Gramext.Stoken pattern
+
+     let slist0sep (x, y) = Gramext.Slist0sep (x, y, false)
+     let slist1sep (x, y) = Gramext.Slist1sep (x, y, false)
+
+  let snterml (x, y) = Gramext.Snterml (x, y)
+  let snterm x = Gramext.Snterm x
+  let sself = Gramext.Sself
+  let snext = Gramext.Snext
+  let slist0 x = Gramext.Slist0 x
+  let slist1 x = Gramext.Slist1 x
+  let sopt x = Gramext.Sopt x
 
-module Symbols = GramextMake(G)
+  let snterml_level = function
+  | Gramext.Snterml (_, l) -> l
+  | _ -> failwith "snterml_level"
+
+end
 
 let camlp4_verbosity silent f x =
   let a = !warning_verbose in
@@ -55,7 +227,7 @@ let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
 (** Binding general entry keys to symbol *)
 
 let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function
-| Stop -> fun f -> G.action (fun loc -> f (to_coqloc loc))
+| Stop -> fun f -> G.action (fun loc -> f (!@ loc))
 | Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x))
 
 let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
@@ -121,10 +293,10 @@ let grammar_delete e reinit (pos,rls) =
     let a = of_coq_assoc a in
     let ext = of_coq_position ext in
     let lev = match pos with
-    | Some (CompatGramext.Level n) -> n
+    | Some (Gramext.Level n) -> n
     | _ -> assert false
     in
-    maybe_uncurry (G.extend e) (Some ext, [Some lev,Some a,[]])
+    (G.extend e) (Some ext) [Some lev,Some a,[]]
   | None -> ()
 
 (** Extension *)
@@ -132,13 +304,13 @@ let grammar_delete e reinit (pos,rls) =
 let grammar_extend e reinit ext =
   let ext = of_coq_extend_statement ext in
   let undo () = grammar_delete e reinit ext in
-  let redo () = camlp4_verbosity false (maybe_uncurry (G.extend e)) ext in
+  let redo () = camlp4_verbosity false (uncurry (G.extend e)) ext in
   camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state;
   redo ()
 
 let grammar_extend_sync e reinit ext =
   camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state;
-  camlp4_verbosity false (maybe_uncurry (G.extend e)) (of_coq_extend_statement ext)
+  camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext)
 
 (** The apparent parser of Coq; encapsulate G to keep track
     of the extensions. *)
@@ -147,13 +319,13 @@ module Gram =
   struct
     include G
     let extend e =
-      maybe_curry
+      curry
 	(fun ext ->
 	   camlp4_state :=
 	     (ByEXTEND ((fun () -> grammar_delete e None ext),
-			(fun () -> maybe_uncurry (G.extend e) ext)))
+			(fun () -> uncurry (G.extend e) ext)))
 	   :: !camlp4_state;
-	   maybe_uncurry (G.extend e) ext)
+	   uncurry (G.extend e) ext)
     let delete_rule e pil =
       (* spiwack: if you use load an ML module which contains GDELETE_RULE
 	  in a section, God kills a kitty. As it would corrupt remove_grammars.
@@ -194,14 +366,14 @@ let eoi_entry en =
   let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
   let act = Gram.action (fun _ x loc -> x) in
-  maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 let map_entry f en =
   let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
   let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
   let act = Gram.action (fun x loc -> f x) in
-  maybe_uncurry (Gram.extend e) (None, make_rule [symbs, act]);
+  uncurry (Gram.extend e) (None, make_rule [symbs, act]);
   e
 
 (* Parse a string, does NOT check if the entire string was read
@@ -345,13 +517,13 @@ module Vernac_ =
     let noedit_mode = gec_vernac "noedit_command"
 
     let () =
-      let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
+      let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
       let act_eoi = Gram.action (fun _ loc -> None) in
       let rule = [
         ([ Symbols.stoken Tok.EOI ], act_eoi);
         ([ Symbols.snterm (Gram.Entry.obj vernac) ], act_vernac );
       ] in
-      maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
+      uncurry (Gram.extend main_entry) (None, make_rule rule)
 
     let command_entry_ref = ref noedit_mode
     let command_entry =
@@ -369,7 +541,7 @@ let epsilon_value f e =
   let r = Rule (Next (Stop, e), fun x _ -> f x) in
   let ext = of_coq_extend_statement (None, [None, None, [r]]) in
   let entry = G.entry_create "epsilon" in
-  let () = maybe_uncurry (G.extend entry) ext in
+  let () = uncurry (G.extend entry) ext in
   try Some (parse_string entry "") with _ -> None
 
 (** Synchronized grammar extensions *)
@@ -418,9 +590,9 @@ let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command ta
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
    grammar rules. *)
-type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.frozen_t
+type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state
 
-let freeze _ : frozen_t = (!grammar_stack, CLexer.freeze ())
+let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ())
 
 (* We compare the current state of the grammar and the state to unfreeze,
    by computing the longest common suffixes *)
@@ -435,7 +607,7 @@ let unfreeze (grams, lex) =
   let n = number_of_entries undo in
   remove_grammars n;
   grammar_stack := common;
-  CLexer.unfreeze lex;
+  CLexer.set_keyword_state lex;
   List.iter extend_dyn_grammar (List.rev_map pi2 redo)
 
 (** No need to provide an init function : the grammar state is
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 6c148d393..4248db697 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -18,7 +18,73 @@ open Genredexpr
 
 (** The parser of Coq *)
 
-module Gram : module type of Compat.GrammarMake(CLexer)
+module Gram : sig
+
+  include Grammar.S with type te = Tok.t
+
+(* Where Grammar.S is
+
+module type S =
+  sig
+    type te = 'x;
+    type parsable = 'x;
+    value parsable : Stream.t char -> parsable;
+    value tokens : string -> list (string * int);
+    value glexer : Plexing.lexer te;
+    value set_algorithm : parse_algorithm -> unit;
+    module Entry :
+      sig
+        type e 'a = 'y;
+        value create : string -> e 'a;
+        value parse : e 'a -> parsable -> 'a;
+        value parse_token : e 'a -> Stream.t te -> 'a;
+        value name : e 'a -> string;
+        value of_parser : string -> (Stream.t te -> 'a) -> e 'a;
+        value print : Format.formatter -> e 'a -> unit;
+        external obj : e 'a -> Gramext.g_entry te = "%identity";
+      end
+    ;
+    module Unsafe :
+      sig
+        value gram_reinit : Plexing.lexer te -> unit;
+        value clear_entry : Entry.e 'a -> unit;
+      end
+    ;
+    value extend :
+      Entry.e 'a -> option Gramext.position ->
+        list
+          (option string * option Gramext.g_assoc *
+           list (list (Gramext.g_symbol te) * Gramext.g_action)) ->
+        unit;
+    value delete_rule : Entry.e 'a -> list (Gramext.g_symbol te) -> unit;
+  end
+
+*)
+
+  type 'a entry = 'a Entry.e
+  type internal_entry = Tok.t Gramext.g_entry
+  type symbol = Tok.t Gramext.g_symbol
+  type action = Gramext.g_action
+  type production_rule = symbol list * action
+  type single_extend_statment =
+      string option * Gramext.g_assoc option * production_rule list
+  type extend_statment =
+      Gramext.position option * single_extend_statment list
+
+  type coq_parsable
+
+  val parsable : ?file:string -> char Stream.t -> coq_parsable
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> coq_parsable -> 'a
+  val entry_print : Format.formatter -> 'a entry -> unit
+  val with_parsable : coq_parsable -> ('a -> 'b) -> 'a -> 'b
+
+  (* Apparently not used *)
+  val srules' : production_rule list -> symbol
+  val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
+
+end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e
 
 (** The parser of Coq is built from three kinds of rule declarations:
 
@@ -242,3 +308,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list
 (** Recover the current stack of grammar extensions. *)
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
+
+(** Location Utils  *)
+val to_coqloc : Ploc.t -> Loc.t
+val (!@) : Ploc.t -> Loc.t