From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 parsing/pcoq.ml4 | 432 ++++++++++++++++++++++++++++++-------------------------
 1 file changed, 237 insertions(+), 195 deletions(-)

(limited to 'parsing/pcoq.ml4')

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ff5213ef..075440f1 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -1,77 +1,96 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
-
-(*i $Id: pcoq.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
+open Compat
+open Tok
 open Util
 open Names
 open Extend
 open Libnames
-open Rawterm
+open Glob_term
 open Topconstr
 open Genarg
 open Tacexpr
 open Extrawit
 open Ppextend
 
-(* The parser of Coq *)
+(** The parser of Coq *)
+
+module G = GrammarMake (Lexer)
+
+(* TODO: this is a workaround, since there isn't such
+   [warning_verbose] in new camlp4. In camlp5, this ref
+   gets hidden by [Gramext.warning_verbose] *)
+let warning_verbose = ref true
 
 IFDEF CAMLP5 THEN
+open Gramext
+ELSE
+open G
+END
 
-module L =
-  struct
-    type te = string * string
-    let lexer = Lexer.lexer
-  end
+(** Compatibility with Camlp5 6.x *)
 
-module G = Grammar.GMake(L)
+IFDEF CAMLP5_6_00 THEN
+let slist0sep x y = Slist0sep (x, y, false)
+let slist1sep x y = Slist1sep (x, y, false)
+ELSE
+let slist0sep x y = Slist0sep (x, y)
+let slist1sep x y = Slist1sep (x, y)
+END
 
+let gram_token_of_token tok =
+IFDEF CAMLP5 THEN
+ Stoken (Tok.to_pattern tok)
 ELSE
+ match tok with
+  | KEYWORD s -> Skeyword s
+  | tok -> Stoken ((=) tok, to_string tok)
+END
 
-module L =
-  struct
-    let lexer = Lexer.lexer
-  end
+let gram_token_of_string s = gram_token_of_token (Lexer.terminal s)
 
-module G = Grammar.Make(L)
+let camlp4_verbosity silent f x =
+  let a = !warning_verbose in
+  warning_verbose := silent;
+  f x;
+  warning_verbose := a
 
-END
+let camlp4_verbose f x = camlp4_verbosity (Flags.is_verbose ()) f x
 
-let grammar_delete e pos reinit rls =
-  List.iter
-    (fun (n,ass,lev) ->
 
-      (* Caveat: deletion is not the converse of extension: when an
-	 empty level is extended, deletion removes the level instead
-	 of keeping it empty. This has an effect on the empty levels 8,
-	 99 and 200. We didn't find a good solution to this problem
-	 (e.g. using G.extend to know if the level exists results in a
-	 printed error message as side effect). As a consequence an
-	 extension at 99 or 8 (and for pattern 200 too) inside a section
-         corrupts the parser. *)
+(** General entry keys *)
 
-      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
-    (List.rev rls);
-  if reinit <> None then
-    let lev = match pos with Some (Gramext.Level n) -> n | _ -> assert false in
-    let pos =
-      if lev = "200" then Gramext.First
-      else Gramext.After (string_of_int (int_of_string lev + 1)) in
-    G.extend e (Some pos) [Some lev,reinit,[]];
+(** This intermediate abstract representation of entries can
+   both be reified into mlexpr for the ML extensions and
+   dynamically interpreted as entries for the Coq level extensions
+*)
+
+type prod_entry_key =
+  | Alist1 of prod_entry_key
+  | Alist1sep of prod_entry_key * string
+  | Alist0 of prod_entry_key
+  | Alist0sep of prod_entry_key * string
+  | Aopt of prod_entry_key
+  | Amodifiers of prod_entry_key
+  | Aself
+  | Anext
+  | Atactic of int
+  | Agram of G.internal_entry
+  | Aentry of string * string
+
+(** [grammar_object] is the superclass of all grammar entries *)
 
-(* grammar_object is the superclass of all grammar entries *)
 module type Gramobj =
 sig
   type grammar_object
-  val weaken_entry : 'a G.Entry.e -> grammar_object G.Entry.e
+  val weaken_entry : 'a G.entry -> grammar_object G.entry
 end
 
 module Gramobj : Gramobj =
@@ -80,9 +99,11 @@ struct
   let weaken_entry e = Obj.magic e
 end
 
+(** Grammar entries with associated types *)
+
 type entry_type = argument_type
 type grammar_object = Gramobj.grammar_object
-type typed_entry = argument_type * grammar_object G.Entry.e
+type typed_entry = argument_type * grammar_object G.entry
 let in_typed_entry t e = (t,Gramobj.weaken_entry e)
 let type_of_typed_entry (t,e) = t
 let object_of_typed_entry (t,e) = e
@@ -91,8 +112,8 @@ let weaken_entry x = Gramobj.weaken_entry x
 module type Gramtypes =
 sig
   open Decl_kinds
-  val inGramObj : 'a raw_abstract_argument_type -> 'a G.Entry.e -> typed_entry
-  val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.Entry.e
+  val inGramObj : 'a raw_abstract_argument_type -> 'a G.entry -> typed_entry
+  val outGramObj : 'a raw_abstract_argument_type -> typed_entry -> 'a G.entry
 end
 
 module Gramtypes : Gramtypes =
@@ -107,82 +128,107 @@ end
 
 open Gramtypes
 
-type camlp4_rule =
-    Compat.token Gramext.g_symbol list * Gramext.g_action
+(** Grammar extensions *)
+
+(** NB: [extend_statment =
+         gram_position option * single_extend_statment list]
+    and [single_extend_statment =
+         string option * gram_assoc option * production_rule list]
+    and [production_rule = symbol list * action]
 
-type camlp4_entry_rules =
-    (* first two parameters are name and assoc iff a level is created *)
-    string option * Gramext.g_assoc option * camlp4_rule list
+    In [single_extend_statement], first two parameters are name and
+    assoc iff a level is created *)
 
 type ext_kind =
   | ByGrammar of
-      grammar_object G.Entry.e * Gramext.position option *
-      camlp4_entry_rules list * Gramext.g_assoc option
-  | ByGEXTEND of (unit -> unit) * (unit -> unit)
+      grammar_object G.entry
+      * gram_assoc option (** for reinitialization if ever needed *)
+      * G.extend_statment
+  | ByEXTEND of (unit -> unit) * (unit -> unit)
+
+(** The list of extensions *)
 
 let camlp4_state = ref []
 
-(* The apparent parser of Coq; encapsulate G to keep track of the
-   extensions. *)
+(** Deletion
+
+   Caveat: deletion is not the converse of extension: when an
+   empty level is extended, deletion removes the level instead
+   of keeping it empty. This has an effect on the empty levels 8,
+   99 and 200. We didn't find a good solution to this problem
+   (e.g. using G.extend to know if the level exists results in a
+   printed error message as side effect). As a consequence an
+   extension at 99 or 8 (and for pattern 200 too) inside a section
+   corrupts the parser. *)
+
+let grammar_delete e reinit (pos,rls) =
+  List.iter
+    (fun (n,ass,lev) ->
+      List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev))
+    (List.rev rls);
+  if reinit <> None then
+    let lev = match pos with Some (Level n) -> n | _ -> assert false in
+    let pos =
+      if lev = "200" then First
+      else After (string_of_int (int_of_string lev + 1)) in
+    maybe_uncurry (G.extend e) (Some pos, [Some lev,reinit,[]])
+
+(** The apparent parser of Coq; encapsulate G to keep track
+    of the extensions. *)
+
 module Gram =
   struct
     include G
-    let extend e pos rls =
-      camlp4_state :=
-      (ByGEXTEND ((fun () -> grammar_delete e pos None rls),
-                  (fun () -> G.extend e pos rls)))
-      :: !camlp4_state;
-      G.extend e pos rls
+    let extend e =
+      maybe_curry
+	(fun ext ->
+	   camlp4_state :=
+	     (ByEXTEND ((fun () -> grammar_delete e None ext),
+			(fun () -> maybe_uncurry (G.extend e) ext)))
+	   :: !camlp4_state;
+	   maybe_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.
           There does not seem to be a good way to undo a delete rule. As deleting
 	  takes fewer arguments than extending. The production rule isn't returned
 	  by delete_rule. If we could retrieve the necessary information, then
-	  ByGEXTEND provides just the framework we need to allow this in section.
+	  ByEXTEND provides just the framework we need to allow this in section.
 	  I'm not entirely sure it makes sense, but at least it would be more correct.
           *)
       G.delete_rule e pil
   end
 
-IFDEF CAMLP5_6_02_1 THEN
-let entry_print x = Gram.Entry.print !Pp_control.std_ft x
-ELSE
-let entry_print = Gram.Entry.print
-END
+(** This extension command is used by the Grammar constr *)
 
-let camlp4_verbosity silent f x =
-  let a = !Gramext.warning_verbose in
-  Gramext.warning_verbose := silent;
-  f x;
-  Gramext.warning_verbose := a
-
-(* This extension command is used by the Grammar constr *)
+let grammar_extend e reinit ext =
+  camlp4_state := ByGrammar (weaken_entry e,reinit,ext) :: !camlp4_state;
+  camlp4_verbose (maybe_uncurry (G.extend e)) ext
 
-let grammar_extend te pos reinit rls =
-  camlp4_state := ByGrammar (weaken_entry te,pos,rls,reinit) :: !camlp4_state;
-  camlp4_verbosity (Flags.is_verbose ()) (G.extend te pos) rls
+(** Remove extensions
 
-(* n is the number of extended entries (not the number of Grammar commands!)
+   [n] is the number of extended entries (not the number of Grammar commands!)
    to remove. *)
+
 let rec remove_grammars n =
   if n>0 then
     (match !camlp4_state with
        | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
-       | ByGrammar(g,pos,rls,reinit)::t ->
-           grammar_delete g pos reinit rls;
+       | ByGrammar(g,reinit,ext)::t ->
+           grammar_delete g reinit ext;
            camlp4_state := t;
            remove_grammars (n-1)
-       | ByGEXTEND (undo,redo)::t ->
+       | ByEXTEND (undo,redo)::t ->
            undo();
            camlp4_state := t;
            remove_grammars n;
            redo();
-           camlp4_state := ByGEXTEND (undo,redo) :: !camlp4_state)
+           camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state)
+
+(** An entry that checks we reached the end of the input. *)
 
-(* An entry that checks we reached the end of the input. *)
 let eoi_entry en =
-  let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_eoi") in
+  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
   GEXTEND Gram
     e: [ [ x = en; EOI -> x ] ]
     ;
@@ -190,7 +236,7 @@ let eoi_entry en =
   e
 
 let map_entry f en =
-  let e = Gram.Entry.create ((Gram.Entry.name en) ^ "_map") in
+  let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
   GEXTEND Gram
     e: [ [ x = en -> f x ] ]
     ;
@@ -201,7 +247,7 @@ let map_entry f en =
    (use eoi_entry) *)
 
 let parse_string f x =
-  let strm = Stream.of_string x in Gram.Entry.parse f (Gram.parsable strm)
+  let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
 
 type gram_universe = string * (string, typed_entry) Hashtbl.t
 
@@ -228,17 +274,10 @@ let get_univ s =
 
 let get_entry (u, utab) s = Hashtbl.find utab s
 
-let get_entry_type (u, utab) s =
-  try
-    type_of_typed_entry (get_entry (u, utab) s)
-  with Not_found ->
-    errorlabstrm "Pcoq.get_entry"
-      (str "Unknown grammar entry " ++ str u ++ str ":" ++ str s ++ str ".")
-
 let new_entry etyp (u, utab) s =
   if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr);
   let ename = u ^ ":" ^ s in
-  let e = in_typed_entry etyp (Gram.Entry.create ename) in
+  let e = in_typed_entry etyp (Gram.entry_create ename) in
   Hashtbl.add utab s e; e
 
 let create_entry (u, utab) s etyp =
@@ -257,10 +296,10 @@ let create_generic_entry s wit =
   outGramObj wit (create_entry utactic s (unquote wit))
 
 (* [make_gen_entry] builds entries extensible by giving its name (a string) *)
-(* For entries extensible only via the ML name, Gram.Entry.create is enough *)
+(* For entries extensible only via the ML name, Gram.entry_create is enough *)
 
 let make_gen_entry (u,univ) rawwit s =
-  let e = Gram.Entry.create (u ^ ":" ^ s) in
+  let e = Gram.entry_create (u ^ ":" ^ s) in
   Hashtbl.add univ s (inGramObj rawwit e); e
 
 (* Initial grammar entries *)
@@ -269,44 +308,43 @@ module Prim =
   struct
     let gec_gen x = make_gen_entry uprim x
 
-    (* Entries that can be refered via the string -> Gram.Entry.e table *)
+    (* Entries that can be refered via the string -> Gram.entry table *)
     (* Typically for tactic or vernac extensions *)
     let preident = gec_gen rawwit_pre_ident "preident"
     let ident = gec_gen rawwit_ident "ident"
     let natural = gec_gen rawwit_int "natural"
     let integer = gec_gen rawwit_int "integer"
-    let bigint = Gram.Entry.create "Prim.bigint"
+    let bigint = Gram.entry_create "Prim.bigint"
     let string = gec_gen rawwit_string "string"
     let reference = make_gen_entry uprim rawwit_ref "reference"
-    let by_notation = Gram.Entry.create "by_notation"
-    let smart_global = Gram.Entry.create "smart_global"
+    let by_notation = Gram.entry_create "by_notation"
+    let smart_global = Gram.entry_create "smart_global"
 
     (* parsed like ident but interpreted as a term *)
     let var = gec_gen rawwit_var "var"
 
-    let name = Gram.Entry.create "Prim.name"
-    let identref = Gram.Entry.create "Prim.identref"
+    let name = Gram.entry_create "Prim.name"
+    let identref = Gram.entry_create "Prim.identref"
     let pattern_ident = gec_gen rawwit_pattern_ident "pattern_ident"
-    let pattern_identref = Gram.Entry.create "pattern_identref"
+    let pattern_identref = Gram.entry_create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
-    let base_ident = Gram.Entry.create "Prim.base_ident"
+    let base_ident = Gram.entry_create "Prim.base_ident"
 
-    let qualid = Gram.Entry.create "Prim.qualid"
-    let fullyqualid = Gram.Entry.create "Prim.fullyqualid"
-    let dirpath = Gram.Entry.create "Prim.dirpath"
+    let qualid = Gram.entry_create "Prim.qualid"
+    let fullyqualid = Gram.entry_create "Prim.fullyqualid"
+    let dirpath = Gram.entry_create "Prim.dirpath"
 
-    let ne_string = Gram.Entry.create "Prim.ne_string"
-    let ne_lstring = Gram.Entry.create "Prim.ne_lstring"
+    let ne_string = Gram.entry_create "Prim.ne_string"
+    let ne_lstring = Gram.entry_create "Prim.ne_lstring"
 
   end
 
 module Constr =
   struct
     let gec_constr = make_gen_entry uconstr rawwit_constr
-    let gec_constr_list = make_gen_entry uconstr (wit_list0 rawwit_constr)
 
-    (* Entries that can be refered via the string -> Gram.Entry.e table *)
+    (* Entries that can be refered via the string -> Gram.entry table *)
     let constr = gec_constr "constr"
     let operconstr = gec_constr "operconstr"
     let constr_eoi = eoi_entry constr
@@ -315,31 +353,31 @@ module Constr =
     let ident = make_gen_entry uconstr rawwit_ident "ident"
     let global = make_gen_entry uconstr rawwit_ref "global"
     let sort = make_gen_entry uconstr rawwit_sort "sort"
-    let pattern = Gram.Entry.create "constr:pattern"
+    let pattern = Gram.entry_create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
-    let closed_binder = Gram.Entry.create "constr:closed_binder"
-    let binder = Gram.Entry.create "constr:binder"
-    let binders = Gram.Entry.create "constr:binders"
-    let open_binders = Gram.Entry.create "constr:open_binders"
-    let binders_fixannot = Gram.Entry.create "constr:binders_fixannot"
-    let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
-    let record_declaration = Gram.Entry.create "constr:record_declaration"
-    let appl_arg = Gram.Entry.create "constr:appl_arg"
+    let closed_binder = Gram.entry_create "constr:closed_binder"
+    let binder = Gram.entry_create "constr:binder"
+    let binders = Gram.entry_create "constr:binders"
+    let open_binders = Gram.entry_create "constr:open_binders"
+    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
+    let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
+    let record_declaration = Gram.entry_create "constr:record_declaration"
+    let appl_arg = Gram.entry_create "constr:appl_arg"
   end
 
 module Module =
   struct
-    let module_expr = Gram.Entry.create "module_expr"
-    let module_type = Gram.Entry.create "module_type"
+    let module_expr = Gram.entry_create "module_expr"
+    let module_type = Gram.entry_create "module_type"
   end
 
 module Tactic =
   struct
     (* Main entry for extensions *)
-    let simple_tactic = Gram.Entry.create "tactic:simple_tactic"
+    let simple_tactic = Gram.entry_create "tactic:simple_tactic"
 
-    (* Entries that can be refered via the string -> Gram.Entry.e table *)
+    (* Entries that can be refered via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
       make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
@@ -358,9 +396,9 @@ module Tactic =
       make_gen_entry utactic rawwit_intro_pattern "simple_intropattern"
 
     (* Main entries for ltac *)
-    let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
-    let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
-    let binder_tactic = Gram.Entry.create "tactic:binder_tactic"
+    let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+    let tactic_expr = Gram.entry_create "tactic:tactic_expr"
+    let binder_tactic = Gram.entry_create "tactic:binder_tactic"
 
     let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
@@ -371,7 +409,7 @@ module Tactic =
 
 module Vernac_ =
   struct
-    let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
+    let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
 
     (* The different kinds of vernacular commands *)
     let gallina = gec_vernac "gallina"
@@ -379,12 +417,11 @@ module Vernac_ =
     let command = gec_vernac "command"
     let syntax = gec_vernac "syntax_command"
     let vernac = gec_vernac "Vernac.vernac"
-    let proof_instr = Gram.Entry.create "proofmode:instr"
-
     let vernac_eoi = eoi_entry vernac
-
+    let rec_definition = gec_vernac "Vernac.rec_definition"
     (* Main vernac entry *)
-    let main_entry = Gram.Entry.create "vernac"
+    let main_entry = Gram.entry_create "vernac"
+
     GEXTEND Gram
     main_entry:
       [ [ a = vernac -> Some (loc,a) | EOI -> None ] ]
@@ -411,23 +448,24 @@ let main_entry = Vernac_.main_entry
 let constr_level = string_of_int
 
 let default_levels =
-  [200,Gramext.RightA,false;
-   100,Gramext.RightA,false;
-   99,Gramext.RightA,true;
-   90,Gramext.RightA,false;
-   10,Gramext.RightA,false;
-   9,Gramext.RightA,false;
-   8,Gramext.RightA,true;
-   1,Gramext.LeftA,false;
-   0,Gramext.RightA,false]
+  [200,RightA,false;
+   100,RightA,false;
+   99,RightA,true;
+   90,RightA,false;
+   10,RightA,false;
+   9,RightA,false;
+   8,RightA,true;
+   1,LeftA,false;
+   0,RightA,false]
 
 let default_pattern_levels =
-  [200,Gramext.RightA,true;
-   100,Gramext.RightA,false;
-   99,Gramext.RightA,true;
-   10,Gramext.LeftA,false;
-   1,Gramext.LeftA,false;
-   0,Gramext.RightA,false]
+  [200,RightA,true;
+   100,RightA,false;
+   99,RightA,true;
+   10,LeftA,false;
+   9,RightA,false;
+   1,LeftA,false;
+   0,RightA,false]
 
 let level_stack =
   ref [(default_levels, default_pattern_levels)]
@@ -438,19 +476,19 @@ let level_stack =
 open Ppextend
 
 let admissible_assoc = function
-  | Gramext.LeftA, Some (Gramext.RightA | Gramext.NonA) -> false
-  | Gramext.RightA, Some Gramext.LeftA -> false
+  | LeftA, Some (RightA | NonA) -> false
+  | RightA, Some LeftA -> false
   | _ -> true
 
 let create_assoc = function
-  | None -> Gramext.RightA
+  | None -> RightA
   | Some a -> a
 
 let error_level_assoc p current expected =
   let pr_assoc = function
-    | Gramext.LeftA -> str "left"
-    | Gramext.RightA -> str "right"
-    | Gramext.NonA -> str "non" in
+    | LeftA -> str "left"
+    | RightA -> str "right"
+    | NonA -> str "non" in
   errorlabstrm ""
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
@@ -484,18 +522,18 @@ let find_position_gen forpat ensure assoc lev =
 	let assoc = create_assoc assoc in
         if !init = None then
 	  (* Create the entry *)
-	  (if !after = None then Some Gramext.First
-	   else Some (Gramext.After (constr_level (Option.get !after)))),
+	  (if !after = None then Some First
+	   else Some (After (constr_level (Option.get !after)))),
 	   Some assoc, Some (constr_level n), None
         else
 	  (* The reinit flag has been updated *)
-	   Some (Gramext.Level (constr_level n)), None, None, !init
+	   Some (Level (constr_level n)), None, None, !init
       with
 	  (* Nothing has changed *)
           Exit ->
             level_stack := current :: !level_stack;
 	    (* Just inherit the existing associativity and name (None) *)
-	    Some (Gramext.Level (constr_level n)), None, None, None
+	    Some (Level (constr_level n)), None, None, None
 
 let remove_levels n =
   level_stack := list_skipn n !level_stack
@@ -524,8 +562,8 @@ let synchronize_level_positions () =
 
 (* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *)
 let camlp4_assoc = function
-  | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA
-  | None | Some Gramext.LeftA -> Gramext.LeftA
+  | Some NonA | Some RightA -> RightA
+  | None | Some LeftA -> LeftA
 
 (* [adjust_level assoc from prod] where [assoc] and [from] are the name
    and associativity of the level where to add the rule; the meaning of
@@ -540,20 +578,20 @@ let adjust_level assoc from = function
   | (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
 (* Compute production name on the right side *)
   (* If NonA or LeftA on the right-hand side, set to NEXT *)
-  | (NumLevel n,BorderProd (Right,Some (Gramext.NonA|Gramext.LeftA))) ->
+  | (NumLevel n,BorderProd (Right,Some (NonA|LeftA))) ->
       Some None
   (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (NumLevel n,BorderProd (Right,Some Gramext.RightA)) ->
+  | (NumLevel n,BorderProd (Right,Some RightA)) ->
       Some (Some (n,true))
 (* Compute production name on the left side *)
   (* If NonA on the left-hand side, adopt the current assoc ?? *)
-  | (NumLevel n,BorderProd (Left,Some Gramext.NonA)) -> None
+  | (NumLevel n,BorderProd (Left,Some NonA)) -> None
   (* If the expected assoc is the current one, set to SELF *)
   | (NumLevel n,BorderProd (Left,Some a)) when a = camlp4_assoc assoc ->
       None
   (* Otherwise, force the level, n or n-1, according to expected assoc *)
   | (NumLevel n,BorderProd (Left,Some a)) ->
-      if a = Gramext.LeftA then Some (Some (n,true)) else Some None
+      if a = LeftA then Some (Some (n,true)) else Some None
   (* None means NEXT *)
   | (NextLevel,_) -> Some None
 (* Compute production name elsewhere *)
@@ -604,7 +642,7 @@ let interp_constr_prod_entry_key ass from forpat en =
 let is_self from e =
   match from, e with
       ETConstr(n,()), ETConstr(NumLevel n',
-        BorderProd(Right, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false
+        BorderProd(Right, _ (* Some(NonA|LeftA) *))) -> false
     | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> n=n'
     | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
       | ETPattern, ETPattern) -> true
@@ -618,69 +656,73 @@ let is_binder_level from e =
     | _ -> false
 
 let make_sep_rules tkl =
-  Gramext.srules
-    [List.map (fun x -> Gramext.Stoken x) tkl,
-     List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl
-       (Gramext.action (fun loc -> ()))]
+  Gram.srules'
+    [List.map gram_token_of_token tkl,
+     List.fold_right (fun _ v -> Gram.action (fun _ -> v)) tkl
+       (Gram.action (fun loc -> ()))]
 
 let rec symbol_of_constr_prod_entry_key assoc from forpat typ =
   if is_binder_level from typ then
     if forpat then
-      Gramext.Snterml (Gram.Entry.obj Constr.pattern,"200")
+      Snterml (Gram.Entry.obj Constr.pattern,"200")
     else
-      Gramext.Snterml (Gram.Entry.obj Constr.operconstr,"200")
+      Snterml (Gram.Entry.obj Constr.operconstr,"200")
   else if is_self from typ then
-    Gramext.Sself
+      Sself
   else
     match typ with
     | ETConstrList (typ',[]) ->
-        Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
+        Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
     | ETConstrList (typ',tkl) ->
-        Compat.slist1sep
+        slist1sep
           (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
           (make_sep_rules tkl)
     | ETBinderList (false,[]) ->
-        Gramext.Slist1
+        Slist1
 	  (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
     | ETBinderList (false,tkl) ->
-        Compat.slist1sep
+        slist1sep
           (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
           (make_sep_rules tkl)
+
     | _ ->
     match interp_constr_prod_entry_key assoc from forpat typ with
-      | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)
-      | (eobj,Some None,_) -> Gramext.Snext
+      | (eobj,None,_) -> Snterm (Gram.Entry.obj eobj)
+      | (eobj,Some None,_) -> Snext
       | (eobj,Some (Some (lev,cur)),_) ->
-          Gramext.Snterml (Gram.Entry.obj eobj,constr_level lev)
+          Snterml (Gram.Entry.obj eobj,constr_level lev)
 
-(**********************************************************************)
-(* Binding general entry keys to symbol                               *)
+(** Binding general entry keys to symbol *)
 
 let rec symbol_of_prod_entry_key = function
-  | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
+  | Alist1 s -> Slist1 (symbol_of_prod_entry_key s)
   | Alist1sep (s,sep) ->
-      Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
-  | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
+      slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
+  | Alist0 s -> Slist0 (symbol_of_prod_entry_key s)
   | Alist0sep (s,sep) ->
-      Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
-  | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
+      slist0sep (symbol_of_prod_entry_key s) (gram_token_of_string sep)
+  | Aopt s -> Sopt (symbol_of_prod_entry_key s)
   | Amodifiers s ->
-       Gramext.srules
-        [([], Gramext.action(fun _loc -> []));
-         ([Gramext.Stoken ("", "(");
-           Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
-           Gramext.Stoken ("", ")")],
-	   Gramext.action (fun _ l _ _loc -> l))]
-  | Aself -> Gramext.Sself
-  | Anext -> Gramext.Snext
-  | Atactic 5 -> Gramext.Snterm (Gram.Entry.obj Tactic.binder_tactic)
+       Gram.srules'
+        [([], Gram.action (fun _loc -> []));
+         ([gram_token_of_string "(";
+           slist1sep (symbol_of_prod_entry_key s) (gram_token_of_string ",");
+           gram_token_of_string ")"],
+	   Gram.action (fun _ l _ _loc -> l))]
+  | Aself -> Sself
+  | Anext -> Snext
+  | Atactic 5 -> Snterm (Gram.Entry.obj Tactic.binder_tactic)
   | Atactic n ->
-      Gramext.Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
-  | Agram s -> Gramext.Snterm s
+      Snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
+  | Agram s -> Snterm s
   | Aentry (u,s) ->
-      Gramext.Snterm (Gram.Entry.obj
+      Snterm (Gram.Entry.obj
 	(object_of_typed_entry (get_entry (get_univ u) s)))
 
+let level_of_snterml = function
+  | Snterml (_,l) -> int_of_string l
+  | _ -> failwith "level_of_snterml"
+
 (**********************************************************************)
 (* Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
-- 
cgit v1.2.3