Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension points of Camlp5

5 files changed, 229 insertions, 207 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index 6805a96edc..f57e32c884 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -101,7 +101,7 @@ type ('self, 'a) symbol =
 | Aself : ('self, 'self) symbol
 | Anext : ('self, 'self) symbol
 | Aentry : 'a entry -> ('self, 'a) symbol
-| Aentryl : 'a entry * int -> ('self, 'a) symbol
+| Aentryl : 'a entry * string -> ('self, 'a) symbol
 | Arules : 'a rules list -> ('self, 'a) symbol
 
 and ('self, _, 'r) rule =
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.mlg
index 1fa26b4556..b2913d5d4f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Names
 open Constr
 open Libnames
@@ -126,396 +128,399 @@ let name_colon =
 
 let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr universe_level sort sort_family
   global constr_pattern lconstr_pattern Constr.ident
   closed_binder open_binders binder binders binders_fixannot
   record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
-    [ [ id = Prim.ident -> id ] ]
+    [ [ id = Prim.ident -> { id } ] ]
   ;
   Prim.name:
-    [ [ "_" -> CAst.make ~loc:!@loc Anonymous ] ]
+    [ [ "_" -> { CAst.make ~loc Anonymous } ] ]
   ;
   global:
-    [ [ r = Prim.reference -> r ] ]
+    [ [ r = Prim.reference -> { r } ] ]
   ;
   constr_pattern:
-    [ [ c = constr -> c ] ]
+    [ [ c = constr -> { c } ] ]
   ;
   lconstr_pattern:
-    [ [ c = lconstr -> c ] ]
+    [ [ c = lconstr -> { c } ] ]
   ;
   sort:
-    [ [ "Set"  -> GSet
-      | "Prop" -> GProp
-      | "Type" -> GType []
-      | "Type"; "@{"; u = universe; "}" -> GType u
+    [ [ "Set"  -> { GSet }
+      | "Prop" -> { GProp }
+      | "Type" -> { GType [] }
+      | "Type"; "@{"; u = universe; "}" -> { GType u }
       ] ]
   ;
   sort_family:
-    [ [ "Set"  -> Sorts.InSet
-      | "Prop" -> Sorts.InProp
-      | "Type" -> Sorts.InType
+    [ [ "Set"  -> { Sorts.InSet }
+      | "Prop" -> { Sorts.InProp }
+      | "Type" -> { Sorts.InType }
       ] ]
   ;
   universe_expr:
-    [ [ id = global; "+"; n = natural -> Some (id,n)
-      | id = global -> Some (id,0)
-      | "_" -> None
+    [ [ id = global; "+"; n = natural -> { Some (id,n) }
+      | id = global -> { Some (id,0) }
+      | "_" -> { None }
     ] ]
   ;
   universe:
-    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> ids
-      | u = universe_expr -> [u]
+    [ [ IDENT "max"; "("; ids = LIST1 universe_expr SEP ","; ")" -> { ids }
+      | u = universe_expr -> { [u] }
       ] ]
   ;
   lconstr:
-    [ [ c = operconstr LEVEL "200" -> c ] ]
+    [ [ c = operconstr LEVEL "200" -> { c } ] ]
   ;
   constr:
-    [ [ c = operconstr LEVEL "8" -> c
-      | "@"; f=global; i = instance -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ]
+    [ [ c = operconstr LEVEL "8" -> { c }
+      | "@"; f=global; i = instance -> { CAst.make ~loc @@ CAppExpl((None,f,i),[]) } ] ]
   ;
   operconstr:
     [ "200" RIGHTA
-      [ c = binder_constr -> c ]
+      [ c = binder_constr -> { c } ]
     | "100" RIGHTA
       [ c1 = operconstr; "<:"; c2 = binder_constr ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2)
+                 { CAst.make ~loc @@ CCast(c1, CastVM c2) }
       | c1 = operconstr; "<:"; c2 = SELF ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2)
+                 { CAst.make ~loc @@ CCast(c1, CastVM c2) }
       | c1 = operconstr; "<<:"; c2 = binder_constr ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2)
+                 { CAst.make ~loc @@ CCast(c1, CastNative c2) }
       | c1 = operconstr; "<<:"; c2 = SELF ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2)
+                 { CAst.make ~loc @@ CCast(c1, CastNative c2) }
       | c1 = operconstr; ":";c2 = binder_constr ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2)
+                 { CAst.make ~loc @@ CCast(c1, CastConv c2) }
       | c1 = operconstr; ":"; c2 = SELF ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2)
+                 { CAst.make ~loc @@ CCast(c1, CastConv c2) }
       | c1 = operconstr; ":>" ->
-                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ]
+                 { CAst.make ~loc @@ CCast(c1, CastCoerce) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args)
-      | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args)
+      [ f=operconstr; args=LIST1 appl_arg -> { CAst.make ~loc @@ CApp((None,f),args) }
+      | "@"; f=global; i = instance; args=LIST0 NEXT -> { CAst.make ~loc @@ CAppExpl((None,f,i),args) }
       | "@"; lid = pattern_identref; args=LIST1 identref ->
-          let { CAst.loc = locid; v = id } = lid in
+        { let { CAst.loc = locid; v = id } = lid in
           let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?loc:x.CAst.loc x.CAst.v, None), None) args in
-          CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ]
+          CAst.make ~loc @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) } ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc ldots_var), None),[c]) ]
+          { CAst.make ~loc @@ CAppExpl ((None, (qualid_of_ident ~loc ldots_var), None),[c]) } ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
-	CAst.make ~loc:(!@loc) @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None])
+	{ CAst.make ~loc @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None]) }
       | c=operconstr; ".("; "@"; f=global;
         args=LIST0 (operconstr LEVEL "9"); ")" ->
-        CAst.make ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c])
-      | c=operconstr; "%"; key=IDENT -> CAst.make ~loc:(!@loc) @@ CDelimiters (key,c) ]
+        { CAst.make ~loc @@ CAppExpl((Some (List.length args+1),f,None),args@[c]) }
+      | c=operconstr; "%"; key=IDENT -> { CAst.make ~loc @@ CDelimiters (key,c) } ]
     | "0"
-      [ c=atomic_constr -> c
-      | c=match_constr -> c
+      [ c=atomic_constr -> { c }
+      | c=match_constr -> { c }
       | "("; c = operconstr LEVEL "200"; ")" ->
-          (match c.CAst.v with
+        { (match c.CAst.v with
             | CPrim (Numeral (n,true)) ->
-                CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[],[]))
-            | _ -> c)
-      | "{|"; c = record_declaration; "|}" -> c
+                CAst.make ~loc @@ CNotation("( _ )",([c],[],[],[]))
+            | _ -> c) }
+      | "{|"; c = record_declaration; "|}" -> { c }
       | "{"; c = binder_constr ; "}" ->
-          CAst.make ~loc:(!@loc) @@ CNotation(("{ _ }"),([c],[],[],[]))
+          { CAst.make ~loc @@ CNotation(("{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
-	  CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
+	  { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
       | "`("; c = operconstr LEVEL "200"; ")" ->
-	  CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c)
+	  { CAst.make ~loc @@ CGeneralization (Explicit, None, c) }
       ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields -> CAst.make ~loc:(!@loc) @@ CRecord fs ] ]
+    [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ]
   ;
 
   record_fields:
-    [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
-      | f = record_field_declaration -> [f]
-      | -> []
+    [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs }
+      | f = record_field_declaration -> { [f] }
+      | -> { [] }
     ] ]
   ;
 
   record_field_declaration:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
-      (id, mkCLambdaN ~loc:!@loc bl c) ] ]
+      { (id, mkCLambdaN ~loc bl c) } ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-          mkCProdN ~loc:!@loc bl c
+          { mkCProdN ~loc bl c }
       | "fun"; bl = open_binders; "=>"; c = operconstr LEVEL "200" ->
-          mkCLambdaN ~loc:!@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 ty,c1 = match ty, c1 with
+        { let ty,c1 = match ty, c1 with
           | (_,None), { CAst.v = CCast(c, CastConv t) } -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
-          CAst.make ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
-                 Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2)
+          CAst.make ~loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
+                 Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) }
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
-          let fixp = mk_single_fix fx in
+          { let fixp = mk_single_fix fx in
           let { CAst.loc = li; v = id } = match fixp.CAst.v with
               CFix(id,_) -> id
             | CCoFix(id,_) -> id
             | _ -> assert false in
-          CAst.make ~loc:!@loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c)
-      | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
+          CAst.make ~loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) }
+      | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> { l } | "()" -> { [] } ];
 	  po = return_type;
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
-          CAst.make ~loc:!@loc @@ CLetTuple (lb,po,c1,c2)
+          { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) }
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, None,    [c1, None, None],       [CAst.make ~loc:!@loc ([[p]], c2)])
+	    { CAst.make ~loc @@
+            CCases (LetPatternStyle, None,    [c1, None, None],       [CAst.make ~loc ([[p]], c2)]) }
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@loc ([[p]], c2)])
+	    { CAst.make ~loc @@
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) }
 
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CAst.make ~loc:!@loc @@
-            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)])
+	    { CAst.make ~loc @@
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc ([[p]], c2)]) }
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
-          CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2)
-      | c=fix_constr -> c ] ]
+          { CAst.make ~loc @@ CIf (c, po, b1, b2) }
+      | c=fix_constr -> { c } ] ]
   ;
   appl_arg:
     [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
-          (c,Some (CAst.make ~loc:!@loc @@ ExplByName id))
-      | c=operconstr LEVEL "9" -> (c,None) ] ]
+          { (c,Some (CAst.make ~loc @@ ExplByName id)) }
+      | c=operconstr LEVEL "9" -> { (c,None) } ] ]
   ;
   atomic_constr:
-    [ [ g=global; i=instance -> CAst.make ~loc:!@loc @@ CRef (g,i)
-      | s=sort   -> CAst.make ~loc:!@loc @@  CSort s
-      | n=INT    -> CAst.make ~loc:!@loc @@ CPrim (Numeral (n,true))
-      | s=string -> CAst.make ~loc:!@loc @@ CPrim (String s)
-      | "_"      -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)
-      | "?"; "["; id=ident; "]"  -> CAst.make ~loc:!@loc @@  CHole (None, IntroIdentifier id, None)
-      | "?"; "["; id=pattern_ident; "]"  -> CAst.make ~loc:!@loc @@  CHole (None, IntroFresh id, None)
-      | id=pattern_ident; inst = evar_instance -> CAst.make ~loc:!@loc @@ CEvar(id,inst) ] ]
+    [ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) }
+      | s=sort   -> { CAst.make ~loc @@  CSort s }
+      | n=INT    -> { CAst.make ~loc @@ CPrim (Numeral (n,true)) }
+      | s=string -> { CAst.make ~loc @@ CPrim (String s) }
+      | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
+      | "?"; "["; id=ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id, None) }
+      | "?"; "["; id=pattern_ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroFresh id, None) }
+      | id=pattern_ident; inst = evar_instance -> { CAst.make ~loc @@ CEvar(id,inst) } ] ]
   ;
   inst:
-    [ [ id = ident; ":="; c = lconstr -> (id,c) ] ]
+    [ [ id = ident; ":="; c = lconstr -> { (id,c) } ] ]
   ;
   evar_instance:
-    [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> l
-      | -> [] ] ]
+    [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> { l }
+      | -> { [] } ] ]
   ;
   instance:
-    [ [ "@{"; l = LIST0 universe_level; "}" -> Some l
-      | -> None ] ]
+    [ [ "@{"; l = LIST0 universe_level; "}" -> { Some l }
+      | -> { None } ] ]
   ;
   universe_level:
-    [ [ "Set" -> GSet
-      | "Prop" -> GProp
-      | "Type" -> GType UUnknown
-      | "_" -> GType UAnonymous
-      | id = global -> GType (UNamed id)
+    [ [ "Set" -> { GSet }
+      | "Prop" -> { GProp }
+      | "Type" -> { GType UUnknown }
+      | "_" -> { GType UAnonymous }
+      | id = global -> { GType (UNamed id) }
       ] ]
   ;
   fix_constr:
-    [ [ fx1=single_fix -> mk_single_fix fx1
-      | (_,kw,dcl1)=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
+    [ [ fx1=single_fix -> { mk_single_fix fx1 }
+      | f=single_fix; "with"; dcls=LIST1 fix_decl SEP "with";
         "for"; id=identref ->
-          mk_fix(!@loc,kw,id,dcl1::dcls)
+          { let (_,kw,dcl1) = f in
+          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
-      | "cofix" -> false ] ]
+    [ [ "fix" -> { true }
+      | "cofix" -> { false } ] ]
   ;
   fix_decl:
     [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
         c=operconstr LEVEL "200" ->
-          (id,fst bl,snd bl,c,ty) ] ]
+          { (id,fst bl,snd bl,c,ty) } ] ]
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
-        br=branches; "end" -> CAst.make ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ]
+        br=branches; "end" -> { CAst.make ~loc @@ CCases(RegularStyle,ty,ci,br) } ] ]
   ;
   case_item:
     [ [ c=operconstr LEVEL "100";
-        ona = OPT ["as"; id=name -> id];
-	ty = OPT ["in"; t=pattern -> t] ->
-	   (c,ona,ty) ] ]
+        ona = OPT ["as"; id=name -> { id } ];
+	ty = OPT ["in"; t=pattern -> { t } ] ->
+	   { (c,ona,ty) } ] ]
   ;
   case_type:
-    [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
+    [ [ "return"; ty = operconstr LEVEL "100" -> { ty } ] ]
   ;
   return_type:
-    [ [ a = OPT [ na = OPT["as"; na=name -> na];
-                  ty = case_type -> (na,ty) ] ->
-        match a with
+    [ [ a = OPT [ na = OPT["as"; na=name -> { na } ];
+                  ty = case_type -> { (na,ty) } ] ->
+        { match a with
           | None -> None, None
-          | Some (na,t) -> (na, Some t)
+          | Some (na,t) -> (na, Some t) }
     ] ]
   ;
   branches:
-    [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
+    [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ]
   ;
   mult_pattern:
-    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ]
+    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ]
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
-        "=>"; rhs = lconstr -> (CAst.make ~loc:!@loc (pll,rhs)) ] ]
+        "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ]
   ;
   record_pattern:
-    [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
+    [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ]
   ;
   record_patterns:
-    [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
-      | p = record_pattern; ";" -> [p]
-      | p = record_pattern-> [p]
-      | -> []
+    [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps }
+      | p = record_pattern; ";" -> { [p] }
+      | p = record_pattern-> { [p] }
+      | -> { [] }
     ] ]
   ;
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
       [ p = pattern; "as"; na = name ->
-        CAst.make ~loc:!@loc @@ CPatAlias (p, na)
-      | p = pattern; lp = LIST1 NEXT -> mkAppPattern ~loc:!@loc p lp
+        { CAst.make ~loc @@ CPatAlias (p, na) }
+      | p = pattern; lp = LIST1 NEXT -> { mkAppPattern ~loc p lp }
       | "@"; r = Prim.reference; lp = LIST0 NEXT ->
-        CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
+        { CAst.make ~loc @@ CPatCstr (r, Some lp, []) } ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ]
+      [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ]
     | "0"
-      [ r = Prim.reference                -> CAst.make ~loc:!@loc @@ CPatAtom (Some r)
-      | "{|"; pat = record_patterns; "|}" -> CAst.make ~loc:!@loc @@ CPatRecord pat
-      | "_" -> CAst.make ~loc:!@loc @@ CPatAtom None
+      [ r = Prim.reference                -> { CAst.make ~loc @@ CPatAtom (Some r) }
+      | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat }
+      | "_" -> { CAst.make ~loc @@ CPatAtom None }
       | "("; p = pattern LEVEL "200"; ")" ->
-          (match p.CAst.v with
+          { (match p.CAst.v with
             | CPatPrim (Numeral (n,true)) ->
-                 CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
-            | _ -> p)
+                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
+            | _ -> p) }
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
-          let p =
+          { let p =
             match p with
             | { CAst.v = CPatPrim (Numeral (n,true)) } ->
-                 CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
+                 CAst.make ~loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
-	  CAst.make ~loc:!@loc @@ CPatCast (p, ty)
-      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (n,true))
-      | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ]
+	  CAst.make ~loc @@ CPatCast (p, ty) }
+      | n = INT    -> { CAst.make ~loc @@ CPatPrim (Numeral (n,true)) }
+      | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   impl_ident_tail:
-    [ [ "}" -> binder_of_name Implicit
+    [ [ "}" -> { binder_of_name Implicit }
     | nal=LIST1 name; ":"; c=lconstr; "}" ->
-        (fun na -> CLocalAssum (na::nal,Default Implicit,c))
+        { (fun na -> CLocalAssum (na::nal,Default Implicit,c)) }
     | nal=LIST1 name; "}" ->
-        (fun na -> CLocalAssum (na::nal,Default Implicit,
-                                CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some !@loc)) @@
-                                CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)))
+        { (fun na -> CLocalAssum (na::nal,Default Implicit,
+                                CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some loc)) @@
+                                CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) }
     | ":"; c=lconstr; "}" ->
-	(fun na -> CLocalAssum ([na],Default Implicit,c))
+	{ (fun na -> CLocalAssum ([na],Default Implicit,c)) }
     ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
-    | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
+    [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) }
+    | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) }
     | "{"; IDENT "measure"; m=constr; id=OPT identref;
-	rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
+	rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) }
     ] ]
   ;
   impl_name_head:
-    [ [ id = impl_ident_head -> (CAst.make ~loc:!@loc @@ Name id) ] ]
+    [ [ id = impl_ident_head -> { CAst.make ~loc @@ Name id } ] ]
   ;
   binders_fixannot:
     [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
-          (assum na :: fst bl), snd bl
-      | f = fixannot -> [], f
-      | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
-      | -> [], (None, CStructRec)
+          { (assum na :: fst bl), snd bl }
+      | f = fixannot -> { [], f }
+      | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
+      | -> { [], (None, CStructRec) }
     ] ]
   ;
   open_binders:
     (* Same as binders but parentheses around a closed binder are optional if
        the latter is unique *)
-    [ [ (* open binder *)
+    [ [
         id = name; idl = LIST0 name; ":"; c = lconstr ->
-          [CLocalAssum (id::idl,Default Explicit,c)]
-	(* binders factorized with open binder *)
+          { [CLocalAssum (id::idl,Default Explicit,c)]
+	(* binders factorized with open binder *) }
       | id = name; idl = LIST0 name; bl = binders ->
-          binders_of_names (id::idl) @ bl
+          { binders_of_names (id::idl) @ bl }
       | id1 = name; ".."; id2 = name ->
-          [CLocalAssum ([id1;(CAst.make ~loc:!@loc (Name ldots_var));id2],
-	                  Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
+          { [CLocalAssum ([id1;(CAst.make ~loc (Name ldots_var));id2],
+	                  Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
       | bl = closed_binder; bl' = binders ->
-	  bl@bl'
+	  { bl@bl' }
     ] ]
   ;
   binders:
-    [ [ l = LIST0 binder -> List.flatten l ] ]
+    [ [ l = LIST0 binder -> { List.flatten l } ] ]
   ;
   binder:
-    [ [ id = name -> [CLocalAssum ([id],Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
-      | bl = closed_binder -> bl ] ]
+    [ [ id = name -> { [CLocalAssum ([id],Default Explicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+      | bl = closed_binder -> { bl } ] ]
   ;
   closed_binder:
     [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
-          [CLocalAssum (id::idl,Default Explicit,c)]
+          { [CLocalAssum (id::idl,Default Explicit,c)] }
       | "("; id=name; ":"; c=lconstr; ")" ->
-          [CLocalAssum ([id],Default Explicit,c)]
+          { [CLocalAssum ([id],Default Explicit,c)] }
       | "("; id=name; ":="; c=lconstr; ")" ->
-          (match c.CAst.v with
+          { (match c.CAst.v with
           | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)]
-          | _ -> [CLocalDef (id,c,None)])
+          | _ -> [CLocalDef (id,c,None)]) }
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [CLocalDef (id,c,Some t)]
+          { [CLocalDef (id,c,Some t)] }
       | "{"; id=name; "}" ->
-          [CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
+          { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
-          [CLocalAssum (id::idl,Default Implicit,c)]
+          { [CLocalAssum (id::idl,Default Implicit,c)] }
       | "{"; id=name; ":"; c=lconstr; "}" ->
-          [CLocalAssum ([id],Default Implicit,c)]
+          { [CLocalAssum ([id],Default Implicit,c)] }
       | "{"; id=name; idl=LIST1 name; "}" ->
-          List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl)
+          { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
       | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-	  List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+	  { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc }
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-	  List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+	  { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc }
       | "'"; p = pattern LEVEL "0" ->
-          let (p, ty) =
+          { let (p, ty) =
             match p.CAst.v with
             | CPatCast (p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
-          [CLocalPattern (CAst.make ~loc:!@loc (p, ty))]
+          [CLocalPattern (CAst.make ~loc (p, ty))] }
     ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@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" ->
-          (CAst.make ~loc:!@loc iid), expl, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> { (CAst.make ~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" ->
+          { (CAst.make ~loc iid), expl, c }
       | c = operconstr LEVEL "200" ->
-          (CAst.make ~loc:!@loc Anonymous), false, c
+          { (CAst.make ~loc Anonymous), false, c }
     ] ]
   ;
 
   type_cstr:
-    [ [ c=OPT [":"; c=lconstr -> c] -> Loc.tag ~loc:!@loc c ] ]
+    [ [ c=OPT [":"; c=lconstr -> { c } ] -> { Loc.tag ~loc c } ] ]
   ;
-  END;;
+  END
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.mlg
index 91dce27fe1..774db97f2c 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+{
+
 open Names
 open Libnames
 
@@ -30,93 +32,96 @@ let my_int_of_string loc s =
   with Failure _ | Exit ->
     CErrors.user_err ~loc  (Pp.str "Cannot support a so large number.")
 
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
   preident:
-    [ [ s = IDENT -> s ] ]
+    [ [ s = IDENT -> { s } ] ]
   ;
   ident:
-    [ [ s = IDENT -> Id.of_string s ] ]
+    [ [ s = IDENT -> { Id.of_string s } ] ]
   ;
   pattern_ident:
-    [ [ LEFTQMARK; id = ident -> id ] ]
+    [ [ LEFTQMARK; id = ident -> { id } ] ]
   ;
   pattern_identref:
-    [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ]
+    [ [ id = pattern_ident -> { CAst.make ~loc id } ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
-    [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
+    [ [ id = ident -> { CAst.make ~loc id } ] ]
   ;
   identref:
-    [ [ id = ident -> CAst.make ~loc:!@loc id ] ]
+    [ [ id = ident -> { CAst.make ~loc id } ] ]
   ;
   field:
-    [ [ s = FIELD -> Id.of_string s ] ]
+    [ [ s = FIELD -> { Id.of_string s } ] ]
   ;
   fields:
-    [ [ id = field; (l,id') = fields -> (l@[id],id')
-      | id = field -> ([],id)
+    [ [ id = field; f = fields -> { let (l,id') = f in (l@[id],id') }
+      | id = field -> { ([],id) }
       ] ]
   ;
   fullyqualid:
-    [ [ id = ident; (l,id')=fields -> CAst.make ~loc:!@loc @@ id::List.rev (id'::l)
-      | id = ident -> CAst.make ~loc:!@loc [id]
+    [ [ id = ident; f=fields -> { let (l,id') = f in CAst.make ~loc @@ id::List.rev (id'::l) }
+      | id = ident -> { CAst.make ~loc [id] }
       ] ]
   ;
   basequalid:
-    [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id'
-      | id = ident -> qualid_of_ident ~loc:!@loc id
+    [ [ id = ident; f=fields -> { let (l,id') = f in  local_make_qualid loc (l@[id]) id' }
+      | id = ident -> { qualid_of_ident ~loc id }
       ] ]
   ;
   name:
-    [ [ IDENT "_"  -> CAst.make ~loc:!@loc Anonymous
-      | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ]
+    [ [ IDENT "_"  -> { CAst.make ~loc Anonymous }
+      | id = ident -> { CAst.make ~loc @@ Name id } ] ]
   ;
   reference:
-    [ [ id = ident; (l,id') = fields ->
-        local_make_qualid !@loc (l@[id]) id'
-      | id = ident -> local_make_qualid !@loc [] id
+    [ [ id = ident; f = fields -> {
+        let (l,id') = f in
+        local_make_qualid loc (l@[id]) id' }
+      | id = ident -> { local_make_qualid loc [] id }
       ] ]
   ;
   by_notation:
-    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ]
+    [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> { key } ] -> { (s, sc) } ] ]
   ;
   smart_global:
-    [ [ c = reference -> CAst.make ~loc:!@loc @@ Constrexpr.AN c
-      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ]
+    [ [ c = reference -> { CAst.make ~loc @@ Constrexpr.AN c }
+      | ntn = by_notation -> { CAst.make ~loc @@ Constrexpr.ByNotation ntn } ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> qid ] ]
+    [ [ qid = basequalid -> { qid } ] ]
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s
+        { if s="" then CErrors.user_err ~loc (Pp.str"Empty string."); s }
     ] ]
   ;
   ne_lstring:
-    [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ]
+    [ [ s = ne_string -> { CAst.make ~loc s } ] ]
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
-        DirPath.make (List.rev (id::l)) ] ]
+        { DirPath.make (List.rev (id::l)) } ] ]
   ;
   string:
-    [ [ s = STRING -> s ] ]
+    [ [ s = STRING -> { s } ] ]
   ;
   lstring:
-    [ [ s = string -> (CAst.make ~loc:!@loc s) ] ]
+    [ [ s = string -> { CAst.make ~loc 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 elsewhere *)
-    [ [ i = INT -> i ] ]
+    [ [ i = INT -> { i } ] ]
   ;
 END
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 6fdd9ea9b9..171276a700 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,9 +17,17 @@ let curry f x y = f (x, y)
 let uncurry f (x,y) = f x y
 
 (** Location Utils  *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
 let coq_file_of_ploc_file s =
   if s = "" then Loc.ToplevelInput else Loc.InFile s
 
+let of_coqloc loc =
+  let open Loc in
+  Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
+
 let to_coqloc loc =
   { Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
     Loc.line_nb = Ploc.line_nb loc;
@@ -236,7 +244,7 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
   | Aentry e ->
     Symbols.snterm (G.Entry.obj e)
   | Aentryl (e, n) ->
-    Symbols.snterml (G.Entry.obj e, string_of_int n)
+    Symbols.snterml (G.Entry.obj e, n)
   | Arules rs ->
     G.srules' (List.map symbol_of_rules rs)
 
@@ -328,6 +336,7 @@ module Gram =
       I'm not entirely sure it makes sense, but at least it would be more correct.
           *)
       G.delete_rule e pil
+    let safe_extend e ext = grammar_extend e None ext
   end
 
 (** Remove extensions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f959bd80c0..48604e1885 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -80,6 +80,8 @@ module type S =
   (* Get comment parsing information from the Lexer *)
   val comment_state : coq_parsable -> ((int * int) * string) list
 
+  val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit
+
   (* Apparently not used *)
   val srules' : production_rule list -> symbol
   val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
@@ -299,6 +301,7 @@ val recover_grammar_command : 'a grammar_command -> 'a list
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 
 (** Location Utils  *)
+val of_coqloc : Loc.t -> Ploc.t
 val to_coqloc : Ploc.t -> Loc.t
 val (!@) : Ploc.t -> Loc.t