Moved Compat to parsing. This permits to break the dependency of the

kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.

This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 500 insertions, 191 deletions

diff --git a/parsing/compat.ml4 b/parsing/compat.ml4
new file mode 100644
index 000000000..9a7c75bcc
--- /dev/null
+++ b/parsing/compat.ml4
@@ -0,0 +1,298 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \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 *)
+
+IFDEF CAMLP5 THEN
+
+module CompatLoc = struct
+  include Ploc
+  let ghost = dummy
+  let merge = encl
+end
+
+exception Exc_located = Ploc.Exc
+
+let of_coqloc loc =
+  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
+  Ploc.make_loc fname lnb pos (bp, ep) ""
+
+let to_coqloc loc =
+  Loc.create (Ploc.file_name loc) (Ploc.line_nb loc)
+    (Ploc.bol_pos loc) (Ploc.first_pos loc, Ploc.last_pos loc)
+
+let make_loc = Ploc.make_unlined
+
+ELSE
+
+module CompatLoc = Camlp4.PreCast.Loc
+
+exception Exc_located = CompatLoc.Exc_located
+
+let of_coqloc loc =
+  let (fname, lnb, pos, bp, ep) = Loc.represent loc in
+  CompatLoc.of_tuple (fname, 0, 0, bp, 0, 0, ep, false)
+
+let to_coqloc loc =
+  Loc.create (CompatLoc.file_name loc) (CompatLoc.start_line loc)
+    (CompatLoc.start_bol loc) (CompatLoc.start_off loc, CompatLoc.stop_off loc)
+
+let make_loc (start, stop) =
+  CompatLoc.of_tuple ("", 0, 0, start, 0, 0, stop, false)
+
+END
+
+let (!@) = to_coqloc
+
+(** Misc module emulation *)
+
+IFDEF CAMLP5 THEN
+
+module PcamlSig = struct end
+module Token = Token
+
+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
+
+END
+
+
+(** Grammar auxiliary types *)
+
+IFDEF CAMLP5 THEN
+
+let to_coq_assoc = function
+| Gramext.RightA -> Extend.RightA
+| Gramext.LeftA -> Extend.LeftA
+| Gramext.NonA -> Extend.NonA
+
+let of_coq_assoc = function
+| Extend.RightA -> Gramext.RightA
+| Extend.LeftA -> Gramext.LeftA
+| Extend.NonA -> Gramext.NonA
+
+let of_coq_position = function
+| 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
+
+let to_coq_position = function
+| Gramext.First -> Extend.First
+| Gramext.Last -> Extend.Last
+| Gramext.Before s -> Extend.Before s
+| Gramext.After s -> Extend.After s
+| Gramext.Level s -> Extend.Level s
+| Gramext.Like _ -> assert false (** dont use it, not in camlp4 *)
+
+ELSE
+
+let to_coq_assoc = function
+| PcamlSig.Grammar.RightA -> Extend.RightA
+| PcamlSig.Grammar.LeftA -> Extend.LeftA
+| PcamlSig.Grammar.NonA -> Extend.NonA
+
+let of_coq_assoc = function
+| Extend.RightA -> PcamlSig.Grammar.RightA
+| Extend.LeftA -> PcamlSig.Grammar.LeftA
+| Extend.NonA -> PcamlSig.Grammar.NonA
+
+let of_coq_position = function
+| Extend.First -> PcamlSig.Grammar.First
+| Extend.Last -> PcamlSig.Grammar.Last
+| Extend.Before s -> PcamlSig.Grammar.Before s
+| Extend.After s -> PcamlSig.Grammar.After s
+| Extend.Level s -> PcamlSig.Grammar.Level s
+
+let to_coq_position = function
+| PcamlSig.Grammar.First -> Extend.First
+| PcamlSig.Grammar.Last -> Extend.Last
+| PcamlSig.Grammar.Before s -> Extend.Before s
+| PcamlSig.Grammar.After s -> Extend.After s
+| PcamlSig.Grammar.Level s -> Extend.Level s
+
+END
+
+
+(** Signature of Lexer *)
+
+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
+end
+
+ELSE
+
+module type LexerSig =
+  Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t
+
+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
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : Format.formatter -> 'a entry -> unit
+  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
+  let action = Gramext.action
+  let entry_create = Entry.create
+  let entry_parse = Entry.parse
+IFDEF CAMLP5_6_02_1 THEN
+  let entry_print ft x = Entry.print ft x
+ELSE
+  let entry_print _ x = Entry.print x
+END
+  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 parsable
+  val parsable : char Stream.t -> parsable
+  val action : 'a -> action
+  val entry_create : string -> 'a entry
+  val entry_parse : 'a entry -> parsable -> 'a
+  val entry_print : Format.formatter -> 'a entry -> unit
+  val srules' : production_rule list -> symbol
+end
+
+module GrammarMake (L:LexerSig) : GrammarSig = struct
+  include Camlp4.Struct.Grammar.Static.Make (L)
+  type 'a entry = 'a Entry.t
+  type action = Action.t
+  type parsable = char Stream.t
+  let parsable s = s
+  let action = Action.mk
+  let entry_create = Entry.mk
+  let entry_parse e s = parse e (*FIXME*)CompatLoc.ghost s
+  let entry_print ft x = Entry.print ft x
+  let srules' = srules (entry_create "dummy")
+end
+
+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
+
+(** Explicit antiquotation $anti:... $ *)
+
+IFDEF CAMLP5 THEN
+let expl_anti loc e = <:expr< $anti:e$ >>
+ELSE
+let expl_anti _loc e = e (* FIXME: understand someday if we can do better *)
+END
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index ade579c69..8f1fda02b 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -184,10 +184,14 @@ let extend_constr (entry,level) (n,assoc) mkact forpat rules =
   let symbs = make_constr_prod_item assoc n forpat pt in
   let pure_sublevels = pure_sublevels level symbs in
   let needed_levels = register_empty_levels forpat pure_sublevels in
+  let map_level (pos, ass1, name, ass2) =
+    (Option.map of_coq_position pos, Option.map of_coq_assoc ass1, name, ass2) in
+  let needed_levels = List.map map_level needed_levels in
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
   let nb_decls = List.length needed_levels + 1 in
   List.iter (prepare_empty_levels forpat) needed_levels;
-  grammar_extend entry reinit (pos,[(name, p4assoc, [symbs, mkact pt])]);
+  grammar_extend entry reinit (Option.map of_coq_position pos,
+    [(name, Option.map of_coq_assoc p4assoc, [symbs, mkact pt])]);
   nb_decls) 0 rules
 
 let extend_constr_notation (n,assoc,ntn,rules) =
@@ -211,7 +215,7 @@ let get_tactic_entry n =
   else if n = 5 then
     weaken_entry Tactic.binder_tactic, None
   else if 1<=n && n<5 then
-    weaken_entry Tactic.tactic_expr, Some (Compat.Level (string_of_int n))
+    weaken_entry Tactic.tactic_expr, Some (Extend.Level (string_of_int n))
   else
     error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
 
@@ -234,7 +238,8 @@ let add_tactic_entry (key,lev,prods,tac) =
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
       make_rule (mkact key tac) prods in
   synchronize_level_positions ();
-  grammar_extend entry None (pos,[(None, None, List.rev [rules])]);
+  grammar_extend entry None (Option.map of_coq_position pos,
+    [(None, None, List.rev [rules])]);
   1
 
 (**********************************************************************)
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 918a36084..0bd8d1990 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -33,7 +33,7 @@ type grammar_constr_prod_item =
        concat with last parsed list if true *)
 
 type notation_grammar =
-    int * gram_assoc option * notation * grammar_constr_prod_item list list
+    int * Extend.gram_assoc option * notation * grammar_constr_prod_item list list
 
 (** Adding notations *)
 
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index c74f36907..735a31f21 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -19,7 +19,7 @@ let make_generic_action
   (f:Loc.t -> ('b * raw_generic_argument) list -> 'a) pil =
   let rec make env = function
     | [] ->
-	Gram.action (fun loc -> f loc env)
+	Gram.action (fun loc -> f (to_coqloc loc) env)
     | None :: tl -> (* parse a non-binding item *)
         Gram.action (fun _ -> make env tl)
     | Some (p, t) :: tl -> (* non-terminal *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 64a8c54ea..1f7a85c8e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -138,7 +138,7 @@ GEXTEND Gram
       | id = METAIDENT -> id_of_string id ] ]
   ;
   Prim.name:
-    [ [ "_" -> (loc, Anonymous) ] ]
+    [ [ "_" -> (!@loc, Anonymous) ] ]
   ;
   global:
     [ [ r = Prim.reference -> r ] ]
@@ -159,54 +159,54 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = operconstr LEVEL "8" -> c
-      | "@"; f=global -> CAppExpl(loc,(None,f),[]) ] ]
+      | "@"; f=global -> CAppExpl(!@loc,(None,f),[]) ] ]
   ;
   operconstr:
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; "<:"; c2 = binder_constr ->
-                 CCast(loc,c1, CastVM c2)
+                 CCast(!@loc,c1, CastVM c2)
       | c1 = operconstr; "<:"; c2 = SELF ->
-                 CCast(loc,c1, CastVM c2)
+                 CCast(!@loc,c1, CastVM c2)
       | c1 = operconstr; ":";c2 = binder_constr ->
-                 CCast(loc,c1, CastConv c2)
+                 CCast(!@loc,c1, CastConv c2)
       | c1 = operconstr; ":"; c2 = SELF ->
-                 CCast(loc,c1, CastConv c2)
+                 CCast(!@loc,c1, CastConv c2)
       | c1 = operconstr; ":>" ->
-                 CCast(loc,c1, CastCoerce) ]
+                 CCast(!@loc,c1, CastCoerce) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
+      [ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args)
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f),args)
       | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
           let args = List.map (fun x -> CRef (Ident x), None) args in
-          CApp(loc,(None,CPatVar(locid,(true,id))),args) ]
+          CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          CAppExpl (loc,(None,Ident (loc,ldots_var)),[c]) ]
+          CAppExpl (!@loc,(None,Ident (!@loc,ldots_var)),[c]) ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
-	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
+	CApp(!@loc,(Some (List.length args+1),CRef f),args@[c,None])
       | c=operconstr; ".("; "@"; f=global;
         args=LIST0 (operconstr LEVEL "9"); ")" ->
-        CAppExpl(loc,(Some (List.length args+1),f),args@[c])
-      | c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
+        CAppExpl(!@loc,(Some (List.length args+1),f),args@[c])
+      | c=operconstr; "%"; key=IDENT -> CDelimiters (!@loc,key,c) ]
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
           (match c with
               CPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CNotation(loc,"( _ )",([c],[],[]))
+                CNotation(!@loc,"( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
-	  CGeneralization (loc, Implicit, None, c)
+	  CGeneralization (!@loc, Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
-	  CGeneralization (loc, Explicit, None, c)
+	  CGeneralization (!@loc, Explicit, None, c)
       ] ]
   ;
   forall:
@@ -216,9 +216,9 @@ GEXTEND Gram
     [ [ "fun" -> () ] ]
   ;
   record_declaration:
-    [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (loc, None, fs)
+    [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
 (*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
-(* 	  CRecord (loc, Some c, fs) *)
+(* 	  CRecord (!@loc, Some c, fs) *)
     ] ]
   ;
   record_field_declaration:
@@ -227,65 +227,65 @@ GEXTEND Gram
   ;
   binder_constr:
     [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          mkCProdN loc bl c
+          mkCProdN (!@loc) bl c
       | lambda; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          mkCLambdaN loc bl c
+          mkCLambdaN (!@loc) bl c
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let loc1 =
 	    Loc.merge (local_binders_loc bl) (constr_loc c1)
 	  in
-          CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+          CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match fixp with
               CFix(_,id,_) -> id
             | CCoFix(_,id,_) -> id
             | _ -> assert false in
-          CLetIn(loc,(li,Name id),fixp,c)
+          CLetIn(!@loc,(li,Name id),fixp,c)
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
-          CLetTuple (loc,lb,po,c1,c2)
+          CLetTuple (!@loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (loc, LetPatternStyle, None, [(c1,(None,None))], [(loc, [(loc,[p])], c2)])
+	    CCases (!@loc, LetPatternStyle, None, [(c1,(None,None))], [(!@loc, [(!@loc,[p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(loc, [(loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, None))], [(!@loc, [(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(loc, [(loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [(c1, (aliasvar p, Some t))], [(!@loc, [(!@loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
-          CIf (loc, c, po, b1, b2)
+          CIf (!@loc, c, po, b1, b2)
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
     [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
-	  (c,Some (loc,ExplByName id))
+	  (c,Some (!@loc,ExplByName id))
       | c=operconstr LEVEL "9" -> (c,None) ] ]
   ;
   atomic_constr:
     [ [ g=global -> CRef g
-      | s=sort -> CSort (loc,s)
-      | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
-      | s=string -> CPrim (loc, String s)
-      | "_" -> CHole (loc, None)
-      | id=pattern_ident -> CPatVar(loc,(false,id)) ] ]
+      | s=sort -> CSort (!@loc,s)
+      | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
+      | s=string -> CPrim (!@loc, String s)
+      | "_" -> CHole (!@loc, None)
+      | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
   ;
   fix_constr:
     [ [ fx1=single_fix -> mk_single_fix fx1
       | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
         "for"; id=identref ->
-          mk_fix(loc,kw,id,dcl1::dcls)
+          mk_fix(!@loc,kw,id,dcl1::dcls)
     ] ]
   ;
   single_fix:
-    [ [ kw=fix_kw; dcl=fix_decl -> (loc,kw,dcl) ] ]
+    [ [ kw=fix_kw; dcl=fix_decl -> (!@loc,kw,dcl) ] ]
   ;
   fix_kw:
     [ [ "fix" -> true
@@ -298,7 +298,7 @@ GEXTEND Gram
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
-        br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ]
+        br=branches; "end" -> CCases(!@loc,RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
     [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
@@ -322,11 +322,11 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   mult_pattern:
-    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (loc,pl) ] ]
+    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (!@loc,pl) ] ]
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
-        "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
+        "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
   ;
   recordpattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
@@ -334,42 +334,42 @@ GEXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (loc,p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
     | "99" RIGHTA [ ]
     | "10" LEFTA
       [ p = pattern; "as"; id = ident ->
-	  CPatAlias (loc, p, id) ]
+	  CPatAlias (!@loc, p, id) ]
     | "9" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
-	  | CPatAtom (_, Some r) -> CPatCstr (loc, r, [], lp)
-	  | CPatCstr (_, r, l1, l2) -> CPatCstr (loc, r, l1 , l2@lp)
-	  | CPatNotation (_, n, s, l) -> CPatNotation (loc, n , s, l@lp)
+	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, [], lp)
+	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
+	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
           | _ -> Errors.user_err_loc
               (cases_pattern_expr_loc p, "compound_pattern",
                Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST1 NEXT ->
-        CPatCstr (loc, r, lp, []) ]
+        CPatCstr (!@loc, r, lp, []) ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
+      [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
-      [ r = Prim.reference -> CPatAtom (loc,Some r)
-      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (loc, pat)
-      | "_" -> CPatAtom (loc,None)
+      [ r = Prim.reference -> CPatAtom (!@loc,Some r)
+      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+      | "_" -> CPatAtom (!@loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
               CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(loc,"( _ )",([p],[]),[])
+                CPatNotation(!@loc,"( _ )",([p],[]),[])
             | _ -> p)
-      | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
-      | s = string -> CPatPrim (loc, String s) ] ]
+      | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
+      | s = string -> CPatPrim (!@loc, String s) ] ]
   ;
   impl_ident_tail:
-    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
+    [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(!@loc, None))
     | idl=LIST1 name; ":"; c=lconstr; "}" ->
         (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
     | idl=LIST1 name; "}" ->
-        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)))
+        (fun id -> LocalRawAssum (id::idl,Default Implicit,CHole (!@loc, None)))
     | ":"; c=lconstr; "}" ->
 	(fun id -> LocalRawAssum ([id],Default Implicit,c))
     ] ]
@@ -383,7 +383,7 @@ GEXTEND Gram
   ;
   binders_fixannot:
     [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot ->
-          (assum (loc, Name id) :: fst bl), snd bl
+          (assum (!@loc, Name id) :: fst bl), snd bl
       | f = fixannot -> [], f
       | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
       | -> [], (None, CStructRec)
@@ -399,8 +399,8 @@ GEXTEND Gram
       | id = name; idl = LIST0 name; bl = binders ->
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
-          [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
-	                  Default Explicit,CHole (loc,None))]
+          [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2],
+	                  Default Explicit,CHole (!@loc,None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
     ] ]
@@ -409,7 +409,7 @@ GEXTEND Gram
     [ [ l = LIST0 binder -> List.flatten l ] ]
   ;
   binder:
-    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None))]
       | bl = closed_binder -> bl ] ]
   ;
   closed_binder:
@@ -420,15 +420,15 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,c)]
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (Loc.merge (constr_loc t) loc,c, CastConv t))]
+          [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))]
       | "{"; id=name; "}" ->
-          [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+          [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
           [LocalRawAssum (id::idl,Default Implicit,c)]
       | "{"; id=name; ":"; c=lconstr; "}" ->
           [LocalRawAssum ([id],Default Implicit,c)]
       | "{"; id=name; idl=LIST1 name; "}" ->
-          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None))) (id::idl)
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
 	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
@@ -436,17 +436,17 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (!@loc, Anonymous), true, c
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
       | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
-	  (loc, iid), expl, c
+	  (!@loc, iid), expl, c
       | c = operconstr LEVEL "200" ->
-	  (loc, Anonymous), false, c
+	  (!@loc, Anonymous), false, c
     ] ]
   ;
 
   type_cstr:
-    [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
+    [ [ c=OPT [":"; c=lconstr -> c] -> (!@loc,c) ] ]
   ;
   END;;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 6506af0a1..7b4628938 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Constrexpr
 open Tacexpr
 open Misctypes
@@ -84,20 +85,20 @@ GEXTEND Gram
       | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
 	  l = LIST0 message_token -> TacFail (n,l)
       | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
-	  TacArg (loc,TacExternal (loc,com,req,la))
-      | st = simple_tactic -> TacAtom (loc,st)
-      | a = may_eval_arg -> TacArg(loc,a)
+	  TacArg (!@loc,TacExternal (!@loc,com,req,la))
+      | st = simple_tactic -> TacAtom (!@loc,st)
+      | a = may_eval_arg -> TacArg(!@loc,a)
       | IDENT "constr"; ":"; id = METAIDENT ->
-          TacArg(loc,MetaIdArg (loc,false,id))
+          TacArg(!@loc,MetaIdArg (!@loc,false,id))
       | IDENT "constr"; ":"; c = Constr.constr ->
-          TacArg(loc,ConstrMayEval(ConstrTerm c))
+          TacArg(!@loc,ConstrMayEval(ConstrTerm c))
       | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
-	  TacArg(loc,IntroPattern ipat)
+	  TacArg(!@loc,IntroPattern ipat)
       | r = reference; la = LIST0 tactic_arg ->
-          TacArg(loc,TacCall (loc,r,la)) ]
+          TacArg(!@loc,TacCall (!@loc,r,la)) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
-      | a = tactic_atom -> TacArg (loc,a) ] ]
+      | a = tactic_atom -> TacArg (!@loc,a) ] ]
   ;
   (* binder_tactic: level 5 of tactic_expr *)
   binder_tactic:
@@ -118,7 +119,7 @@ GEXTEND Gram
       | r = reference -> Reference r
       | c = Constr.constr -> ConstrMayEval (ConstrTerm c)
       (* Unambigous entries: tolerated w/o "ltac:" modifier *)
-      | id = METAIDENT -> MetaIdArg (loc,true,id)
+      | id = METAIDENT -> MetaIdArg (!@loc,true,id)
       | "()" -> TacVoid ] ]
   ;
   may_eval_arg:
@@ -126,7 +127,7 @@ GEXTEND Gram
       | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ]
   ;
   fresh_id:
-    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ]
+    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (!@loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -141,9 +142,9 @@ GEXTEND Gram
       | c = Constr.constr -> ConstrTerm c ] ]
   ;
   tactic_atom:
-    [ [ id = METAIDENT -> MetaIdArg (loc,true,id)
+    [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id)
       | n = integer -> Integer n
-      | r = reference -> TacCall (loc,r,[])
+      | r = reference -> TacCall (!@loc,r,[])
       | "()" -> TacVoid ] ]
   ;
   match_key:
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 55f4a77fb..e868bc77c 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Names
 open Libnames
 open Tok
@@ -44,13 +45,13 @@ GEXTEND Gram
     [ [ LEFTQMARK; id = ident -> id ] ]
   ;
   pattern_identref:
-    [ [ id = pattern_ident -> (loc, id) ] ]
+    [ [ id = pattern_ident -> (!@loc, id) ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
-    [ [ id = ident -> (loc,id) ] ]
+    [ [ id = ident -> (!@loc, id) ] ]
   ;
   identref:
-    [ [ id = ident -> (loc,id) ] ]
+    [ [ id = ident -> (!@loc, id) ] ]
   ;
   field:
     [ [ s = FIELD -> id_of_string s ] ]
@@ -61,8 +62,8 @@ GEXTEND Gram
       ] ]
   ;
   fullyqualid:
-    [ [ id = ident; (l,id')=fields -> loc,id::List.rev (id'::l)
-      | id = ident -> loc,[id]
+    [ [ id = ident; (l,id')=fields -> !@loc,id::List.rev (id'::l)
+      | id = ident -> !@loc,[id]
       ] ]
   ;
   basequalid:
@@ -71,32 +72,32 @@ GEXTEND Gram
       ] ]
   ;
   name:
-    [ [ IDENT "_" -> (loc, Anonymous)
-      | id = ident -> (loc, Name id) ] ]
+    [ [ IDENT "_" -> (!@loc, Anonymous)
+      | id = ident -> (!@loc, Name id) ] ]
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Qualid (loc, local_make_qualid (l@[id]) id')
-      | id = ident -> Ident (loc,id)
+        Qualid (!@loc, local_make_qualid (l@[id]) id')
+      | id = ident -> Ident (!@loc,id)
       ] ]
   ;
   by_notation:
-    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ]
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (!@loc, s, sc) ] ]
   ;
   smart_global:
     [ [ c = reference -> Misctypes.AN c
       | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> loc, qid ] ]
+    [ [ qid = basequalid -> !@loc, qid ] ]
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then Errors.user_err_loc(loc,"",Pp.str"Empty string."); s
+        if s="" then Errors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
-    [ [ s = ne_string -> (loc,s) ] ]
+    [ [ s = ne_string -> (!@loc, s) ] ]
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
@@ -106,11 +107,11 @@ GEXTEND Gram
     [ [ s = STRING -> s ] ]
   ;
   integer:
-    [ [ i = INT      -> my_int_of_string loc i
-      | "-"; i = INT -> - my_int_of_string loc i ] ]
+    [ [ i = INT      -> my_int_of_string (!@loc) i
+      | "-"; i = INT -> - my_int_of_string (!@loc) i ] ]
   ;
   natural:
-    [ [ i = INT -> my_int_of_string loc i ] ]
+    [ [ i = INT -> my_int_of_string (!@loc) i ] ]
   ;
   bigint: (* Negative numbers are dealt with specially *)
     [ [ i = INT -> (Bigint.of_string i) ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index d6592397a..eee6d3ce6 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Constrexpr
 open Vernacexpr
 open Locality
@@ -113,6 +114,6 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
   ;
 END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f62be2f5c..b21711d32 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -218,7 +218,7 @@ GEXTEND Gram
     [ [ id = identref -> AI id
 
       (* This is used in quotations *)
-      | id = METAIDENT -> MetaId (loc,id) ] ]
+      | id = METAIDENT -> MetaId (!@loc, id) ] ]
   ;
   open_constr:
     [ [ c = constr -> ((),c) ] ]
@@ -260,37 +260,37 @@ GEXTEND Gram
     [ [ l = LIST0 simple_intropattern -> l ]]
   ;
   disjunctive_intropattern:
-    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> loc,IntroOrAndPattern tc
-      | "()" -> loc,IntroOrAndPattern [[]]
-      | "("; si = simple_intropattern; ")" -> loc,IntroOrAndPattern [[si]]
+    [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> !@loc,IntroOrAndPattern tc
+      | "()" -> !@loc,IntroOrAndPattern [[]]
+      | "("; si = simple_intropattern; ")" -> !@loc,IntroOrAndPattern [[si]]
       | "("; si = simple_intropattern; ",";
              tc = LIST1 simple_intropattern SEP "," ; ")" ->
-	       loc,IntroOrAndPattern [si::tc]
+	       !@loc,IntroOrAndPattern [si::tc]
       | "("; si = simple_intropattern; "&";
 	     tc = LIST1 simple_intropattern SEP "&" ; ")" ->
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function
 	    | ([]|[_]|[_;_]) as l -> IntroOrAndPattern [l]
 	    | t::q -> IntroOrAndPattern [[t;(loc_of_ne_list q,pairify q)]]
-	  in loc,pairify (si::tc) ] ]
+	  in !@loc,pairify (si::tc) ] ]
   ;
   naming_intropattern:
-    [ [ prefix = pattern_ident -> loc, IntroFresh prefix
-      | "?" -> loc, IntroAnonymous
-      | id = ident -> loc, IntroIdentifier id
-      | "*" -> loc, IntroForthcoming true
-      | "**" -> loc, IntroForthcoming false ] ]
+    [ [ prefix = pattern_ident -> !@loc, IntroFresh prefix
+      | "?" -> !@loc, IntroAnonymous
+      | id = ident -> !@loc, IntroIdentifier id
+      | "*" -> !@loc, IntroForthcoming true
+      | "**" -> !@loc, IntroForthcoming false ] ]
   ;
   simple_intropattern:
     [ [ pat = disjunctive_intropattern -> pat
       | pat = naming_intropattern -> pat
-      | "_" -> loc, IntroWildcard
-      | "->" -> loc, IntroRewrite true
-      | "<-" -> loc, IntroRewrite false ] ]
+      | "_" -> !@loc, IntroWildcard
+      | "->" -> !@loc, IntroRewrite true
+      | "<-" -> !@loc, IntroRewrite false ] ]
   ;
   simple_binding:
-    [ [ "("; id = ident; ":="; c = lconstr; ")" -> (loc, NamedHyp id, c)
-      | "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ]
+    [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c)
+      | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ]
   ;
   bindings:
     [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
@@ -402,13 +402,13 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit,CHole (loc, None))
+    [ [ na=name -> ([na],Default Explicit,CHole (!@loc, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
   fixdecl:
     [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
-        ":"; ty=lconstr; ")" -> (loc,id,bl,ann,ty) ] ]
+        ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ]
   ;
   fixannot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
@@ -416,7 +416,7 @@ GEXTEND Gram
   ;
   cofixdecl:
     [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" ->
-        (loc,id,bl,None,ty) ] ]
+        (!@loc, id, bl, None, ty) ] ]
   ;
   bindings_with_parameters:
     [ [ check_for_coloneq; "(";  id = ident; bl = LIST0 simple_binder;
@@ -459,7 +459,7 @@ GEXTEND Gram
         msg_warning (strbrk msg); Some id
       | IDENT "_eqn" ->
         let msg = "Obsolete syntax \"_eqn\" could be replaced by \"eqn:?\"" in
-        msg_warning (strbrk msg); Some (loc, IntroAnonymous)
+        msg_warning (strbrk msg); Some (!@loc, IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
@@ -558,10 +558,10 @@ GEXTEND Gram
       (* Begin compatibility *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAssert (None,Some (loc,IntroIdentifier id),c)
+	  TacAssert (None,Some (!@loc,IntroIdentifier id),c)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAssert (Some tac,Some (loc,IntroIdentifier id),c)
+	  TacAssert (Some tac,Some (!@loc,IntroIdentifier id),c)
       (* End compatibility *)
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
@@ -674,7 +674,7 @@ GEXTEND Gram
       | r = red_tactic; cl = clause_dft_concl -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
-	  let p,cl = merge_occurrences loc cl oc in
+	  let p,cl = merge_occurrences (!@loc) cl oc in
 	  TacChange (p,c,cl)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 6d82a6504..0519bee8c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -94,8 +94,8 @@ GEXTEND Gram
     [ [ prfcom = default_command_entry -> prfcom ] ]
   ;
   locality:
-    [ [ IDENT "Local" -> locality_flag := Some (loc,true)
-      | IDENT "Global" -> locality_flag := Some (loc,false)
+    [ [ IDENT "Local" -> locality_flag := Some (!@loc,true)
+      | IDENT "Global" -> locality_flag := Some (!@loc,false)
       | -> locality_flag := None ] ]
   ;
   noedit_mode:
@@ -127,7 +127,7 @@ GEXTEND Gram
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
   located_vernac:
-    [ [ v = vernac -> loc, v ] ]
+    [ [ v = vernac -> !@loc, v ] ]
   ;
 END
 
@@ -299,7 +299,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> CHole (loc, None) ] ]
+      | -> CHole (!@loc, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -336,19 +336,19 @@ GEXTEND Gram
   ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
-         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t))
+         t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))
       | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> fun id ->
-	   (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
+	   (oc,DefExpr (id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t)))
       | l = binders; ":="; b = lconstr -> fun id ->
          match b with
 	 | CCast(_,b, (CastConv t|CastVM t)) ->
-	     (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
+	     (None,DefExpr(id,mkCLambdaN (!@loc) l b,Some (mkCProdN (!@loc) l t)))
          | _ ->
-	     (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
+	     (None,DefExpr(id,mkCLambdaN (!@loc) l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id,CHole (loc, None)))
+    [ [ id = name -> (None,AssumExpr(id,CHole (!@loc, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -365,9 +365,9 @@ GEXTEND Gram
   constructor_type:
     [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
-	            fun l id -> (coe <> None,(id,mkCProdN loc l c))
+	            fun l id -> (coe <> None,(id,mkCProdN (!@loc) l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ]
+		 fun l id -> (false,(id,mkCProdN (!@loc) l (CHole (!@loc, None)))) ]
 	 -> t l
      ]]
 ;
@@ -489,7 +489,7 @@ GEXTEND Gram
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CMapply (loc,me1,me2)
+      | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2)
       ] ]
   ;
   module_expr_atom:
@@ -505,9 +505,9 @@ GEXTEND Gram
   module_type:
     [ [ qid = qualid -> CMident qid
       | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me)
+      | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me)
       | mty = module_type; "with"; decl = with_declaration ->
-          CMwith (loc,mty,decl)
+          CMwith (!@loc,mty,decl)
       ] ]
   ;
 END
@@ -589,17 +589,17 @@ GEXTEND Gram
         | "/" -> [`Slash]
         | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
             let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
             List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items
         | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
             let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
             List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items
         | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
             let f x = match sc, x with
-            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
             | Some _, Some _ -> error "scope declared twice" in
             List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items
         ] -> l ] SEP ",";
@@ -677,7 +677,7 @@ GEXTEND Gram
   ;
   argument_spec: [
        [ b = OPT "!"; id = name ; s = OPT scope ->
-       snd id, b <> None, Option.map (fun x -> loc, x) s
+       snd id, b <> None, Option.map (fun x -> !@loc, x) s
     ]
   ];
   strategy_level:
@@ -691,7 +691,7 @@ GEXTEND Gram
     [ [ name = identref; sup = OPT binders ->
 	  (let (loc,id) = name in (loc, Name id)),
           (Option.default [] sup)
-      | -> (loc, Anonymous), []  ] ]
+      | -> (!@loc, Anonymous), []  ] ]
   ;
   reserv_list:
     [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
@@ -1039,7 +1039,7 @@ GEXTEND Gram
         SetOnlyParsing Flags.Current
       | IDENT "compat"; s = STRING ->
         SetOnlyParsing (Coqinit.get_compat_version s)
-      | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s
+      | IDENT "format"; s = [s = STRING -> (!@loc,s)] -> SetFormat s
       | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at";
         lev = level -> SetItemLevel (x::l,lev)
       | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev)
@@ -1057,6 +1057,6 @@ GEXTEND Gram
     [ [ s = ne_string -> TacTerm s
       | nt = IDENT;
         po = OPT [ "("; p = ident; sep = [ -> "" | ","; sep = STRING -> sep ];
-                   ")" -> (p,sep) ] -> TacNonTerm (loc,nt,po) ] ]
+                   ")" -> (p,sep) ] -> TacNonTerm (!@loc,nt,po) ] ]
   ;
 END
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 37d2b332d..29b3579f0 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Compat
 open Pp
 open Errors
 open Util
@@ -44,14 +45,14 @@ GEXTEND Gram
   xml:
     [ [ "<"; otag = IDENT; attrs = LIST0 attr; ">"; l = LIST1 xml;
         "<"; "/"; ctag = IDENT; ">"  ->
-	  check_tags loc otag ctag;
-	  XmlTag (loc,ctag,attrs,l)
+	  check_tags (!@loc) otag ctag;
+	  XmlTag (!@loc,ctag,attrs,l)
       | "<"; tag = IDENT; attrs = LIST0 attr; "/"; ">" ->
-	  XmlTag (loc,tag,attrs,[])
+	  XmlTag (!@loc,tag,attrs,[])
     ] ]
   ;
   attr:
-    [ [ name = IDENT; "="; data = STRING -> (name, (loc, data)) ] ]
+    [ [ name = IDENT; "="; data = STRING -> (name, (!@loc, data)) ] ]
   ;
 END
 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index dc120bd6d..ca5c20c71 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -100,7 +100,7 @@ module Error = struct
 end
 open Error
 
-let err loc str = Loc.raise (make_loc loc) (Error.E str)
+let err loc str = Loc.raise (Loc.make_loc loc) (Error.E str)
 
 let bad_token str = raise (Error.E (Bad_token str))
 
@@ -172,7 +172,7 @@ let lookup_utf8 cs =
     | None -> EmptyStream
 
 let unlocated f x =
-  try f x with Loc.Exc_located (_,exc) -> raise exc
+  try f x with Loc.Exc_located (_, exc) -> raise exc
 
 let check_keyword str =
   let rec loop_symb = parser
@@ -538,7 +538,7 @@ let loct_add loct i loc = Hashtbl.add loct i loc
 
 let current_location_table = ref (loct_create ())
 
-type location_table = (int, Loc.t) Hashtbl.t
+type location_table = (int, CompatLoc.t) Hashtbl.t
 let location_table () = !current_location_table
 let restore_location_table t = current_location_table := t
 let location_function n = loct_func !current_location_table n
@@ -596,10 +596,10 @@ ELSE (* official camlp4 for ocaml >= 3.10 *)
 
 module M_ = Camlp4.ErrorHandler.Register (Error)
 
-module Loc = Loc
+module Loc = CompatLoc
 module Token = struct
   include Tok (* Cf. tok.ml *)
-  module Loc = Loc
+  module Loc = CompatLoc
   module Error = Camlp4.Struct.EmptyError
   module Filter = struct
     type token_filter = (Tok.t * Loc.t) Stream.t -> (Tok.t * Loc.t) Stream.t
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index e5b8ebb11..0e53bd615 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -12,7 +12,7 @@ val add_keyword : string -> unit
 val remove_keyword : string -> unit
 val is_keyword : string -> bool
 
-val location_function : int -> Loc.t
+(* val location_function : int -> Loc.t *)
 
 (** for coqdoc *)
 type location_table
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 98ba1f762..2f0851164 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,4 +1,5 @@
 Tok
+Compat
 Lexer
 Extrawit
 Pcoq
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 04b5e4673..b14822b8a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -28,6 +28,7 @@ let warning_verbose = ref true
 IFDEF CAMLP5 THEN
 open Gramext
 ELSE
+open PcamlSig.Grammar
 open G
 END
 
@@ -210,7 +211,7 @@ let rec remove_grammars n =
     (match !camlp4_state with
        | [] -> anomaly "Pcoq.remove_grammars: too many rules to remove"
        | ByGrammar(g,reinit,ext)::t ->
-           grammar_delete g reinit ext;
+           grammar_delete g (Option.map of_coq_assoc reinit) ext;
            camlp4_state := t;
            remove_grammars (n-1)
        | ByEXTEND (undo,redo)::t ->
@@ -422,7 +423,7 @@ module Vernac_ =
 
     GEXTEND Gram
     main_entry:
-      [ [ a = vernac -> Some (loc,a) | EOI -> None ] ]
+      [ [ a = vernac -> Some (!@loc, a) | EOI -> None ] ]
     ;
     END
 
@@ -446,23 +447,23 @@ let main_entry = Vernac_.main_entry
 let constr_level = string_of_int
 
 let default_levels =
-  [200,RightA,false;
-   100,RightA,false;
-   99,RightA,true;
-   10,RightA,false;
-   9,RightA,false;
-   8,RightA,true;
-   1,LeftA,false;
-   0,RightA,false]
+  [200,Extend.RightA,false;
+   100,Extend.RightA,false;
+   99,Extend.RightA,true;
+   10,Extend.RightA,false;
+   9,Extend.RightA,false;
+   8,Extend.RightA,true;
+   1,Extend.LeftA,false;
+   0,Extend.RightA,false]
 
 let default_pattern_levels =
-  [200,RightA,true;
-   100,RightA,false;
-   99,RightA,true;
-   10,LeftA,false;
-   9,RightA,false;
-   1,LeftA,false;
-   0,RightA,false]
+  [200,Extend.RightA,true;
+   100,Extend.RightA,false;
+   99,Extend.RightA,true;
+   10,Extend.LeftA,false;
+   9,Extend.RightA,false;
+   1,Extend.LeftA,false;
+   0,Extend.RightA,false]
 
 let level_stack =
   ref [(default_levels, default_pattern_levels)]
@@ -472,19 +473,19 @@ let level_stack =
 (* first LeftA, then RightA and NoneA together *)
 
 let admissible_assoc = function
-  | LeftA, Some (RightA | NonA) -> false
-  | RightA, Some LeftA -> false
+  | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
+  | Extend.RightA, Some Extend.LeftA -> false
   | _ -> true
 
 let create_assoc = function
-  | None -> RightA
+  | None -> Extend.RightA
   | Some a -> a
 
 let error_level_assoc p current expected =
   let pr_assoc = function
-    | LeftA -> str "left"
-    | RightA -> str "right"
-    | NonA -> str "non" in
+    | Extend.LeftA -> str "left"
+    | Extend.RightA -> str "right"
+    | Extend.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 " ++
@@ -518,18 +519,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 First
-	   else Some (After (constr_level (Option.get !after)))),
+	  (if !after = None then Some Extend.First
+	   else Some (Extend.After (constr_level (Option.get !after)))),
 	   Some assoc, Some (constr_level n), None
         else
 	  (* The reinit flag has been updated *)
-	   Some (Level (constr_level n)), None, None, !init
+	   Some (Extend.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 (Level (constr_level n)), None, None, None
+	    Some (Extend.Level (constr_level n)), None, None, None
 
 let remove_levels n =
   level_stack := List.skipn n !level_stack
@@ -561,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 NonA | Some RightA -> RightA
-  | None | Some LeftA -> LeftA
+  | Some Extend.NonA | Some Extend.RightA -> Extend.RightA
+  | None | Some Extend.LeftA -> Extend.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
@@ -577,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 (NonA|LeftA))) ->
+  | (NumLevel n,BorderProd (Right,Some (Extend.NonA|Extend.LeftA))) ->
       Some None
   (* If RightA on the right-hand side, set to the explicit (current) level *)
-  | (NumLevel n,BorderProd (Right,Some RightA)) ->
+  | (NumLevel n,BorderProd (Right,Some Extend.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 NonA)) -> None
+  | (NumLevel n,BorderProd (Left,Some Extend.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 = LeftA then Some (Some (n,true)) else Some None
+      if a = Extend.LeftA then Some (Some (n,true)) else Some None
   (* None means NEXT *)
   | (NextLevel,_) -> Some None
 (* Compute production name elsewhere *)
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 682474c51..e9b504e05 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -290,15 +290,15 @@ val interp_entry_name : bool (** true to fail on unknown entry *) ->
 
 val find_position :
   bool (** true if for creation in pattern entry; false if in constr entry *) ->
-  gram_assoc option -> int option ->
-    gram_position option * gram_assoc option * string option *
-    (** for reinitialization: *) gram_assoc option
+  Extend.gram_assoc option -> int option ->
+    Extend.gram_position option * Extend.gram_assoc option * string option *
+    (** for reinitialization: *) Extend.gram_assoc option
 
 val synchronize_level_positions : unit -> unit
 
 val register_empty_levels : bool -> int list ->
-    (gram_position option * gram_assoc option *
-     string option * gram_assoc option) list
+    (Extend.gram_position option * Extend.gram_assoc option *
+     string option * Extend.gram_assoc option) list
 
 val remove_levels : int -> unit