[location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.

4 files changed, 90 insertions, 90 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 49bf267db..712d10a96 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -313,11 +313,11 @@ let interp_entry forpat e = match e with
 | ETBinderList (true, _) -> assert false
 | ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
 
-let constr_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
+let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
   | Name id   -> CRef (Ident (Loc.tag ?loc id), None)
 
-let cases_pattern_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
+let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
   | Name id   -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
 
@@ -342,13 +342,13 @@ match e with
 | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
-  | ForConstr ->  push_constr subst (Loc.tag @@ CPrim (Numeral v))
-  | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral v))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral v))
   end
 | TTReference ->
   begin match forpat with
-  | ForConstr  -> push_constr subst (Loc.tag @@ CRef (v, None))
-  | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v))
+  | ForConstr  -> push_constr subst (CAst.make @@ CRef (v, None))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatAtom (Some v))
   end
 | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
 
@@ -431,12 +431,12 @@ let rec pure_sublevels : type a b c. int option -> (a, b, c) rule -> int list =
 let make_act : type r. r target -> _ -> r gen_eval = function
 | ForConstr -> fun notation loc env ->
   let env = (env.constrs, env.constrlists, List.map fst env.binders) in
-  Loc.tag ~loc @@ CNotation (notation , env)
+  CAst.make ~loc @@ CNotation (notation , env)
 | ForPattern -> fun notation loc env ->
   let invalid = List.exists (fun (_, b) -> not b) env.binders in
   let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
-  Loc.tag ~loc @@ CPatNotation (notation, env, [])
+  CAst.make ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
   let n = ng.notgram_level in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 45585d9ce..a44aa5400 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -34,11 +34,11 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
     let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
-    in Loc.tag ?loc @@ CCast(c, CastConv ty)
+    in CAst.make ?loc @@ CCast(c, CastConv ty)
 
 let binder_of_name expl (loc,na) =
   CLocalAssum ([loc, na], Default expl,
-    Loc.tag ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
+    CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
 
 let binders_of_names l =
   List.map (binder_of_name Explicit) l
@@ -46,7 +46,7 @@ let binders_of_names l =
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let ty = match tyc with
       Some ty -> ty
-    | None    -> Loc.tag @@ CHole (None, IntroAnonymous, None) in
+    | None    -> CAst.make @@ CHole (None, IntroAnonymous, None) in
   (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
@@ -56,16 +56,16 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
       (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
-    | None -> Loc.tag @@ CHole (None, IntroAnonymous, None) in
+    | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
   (id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
   if kw then
     let fb = List.map mk_fixb dcls in
-    Loc.tag ~loc @@ CFix(id,fb)
+    CAst.make ~loc @@ CFix(id,fb)
   else
     let fb = List.map mk_cofixb dcls in
-    Loc.tag ~loc @@ CCoFix(id,fb)
+    CAst.make ~loc @@ CCoFix(id,fb)
 
 let mk_single_fix (loc,kw,dcl) =
   let (id,_,_,_,_) = dcl in mk_fix(loc,kw,id,[dcl])
@@ -120,7 +120,7 @@ let name_colon =
               | _ -> err ())
         | _ -> err ())
 
-let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None
+let aliasvar = function { CAst.loc = loc; CAst.v = CPatAlias (_, id) } -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
@@ -159,62 +159,62 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = operconstr LEVEL "8" -> c
-      | "@"; f=global; i = instance -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ]
+      | "@"; f=global; i = instance -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),[]) ] ]
   ;
   operconstr:
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; "<:"; c2 = binder_constr ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2)
       | c1 = operconstr; "<:"; c2 = SELF ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastVM c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastVM c2)
       | c1 = operconstr; "<<:"; c2 = binder_constr ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2)
       | c1 = operconstr; "<<:"; c2 = SELF ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastNative c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastNative c2)
       | c1 = operconstr; ":";c2 = binder_constr ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2)
       | c1 = operconstr; ":"; c2 = SELF ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastConv c2)
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastConv c2)
       | c1 = operconstr; ":>" ->
-                 Loc.tag ~loc:(!@loc) @@ CCast(c1, CastCoerce) ]
+                 CAst.make ~loc:(!@loc) @@ CCast(c1, CastCoerce) ]
     | "99" RIGHTA [ ]
     | "90" RIGHTA [ ]
     | "10" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> Loc.tag ~loc:(!@loc) @@ CApp((None,f),args)
-      | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),args)
+      [ 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)
       | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
-          let args = List.map (fun x -> Loc.tag @@ CRef (Ident x,None), None) args in
-          Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ?loc:locid @@ CPatVar id),args) ]
+          let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in
+          CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          Loc.tag ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ]
+          CAst.make ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
-	Loc.tag ~loc:(!@loc) @@ CApp((Some (List.length args+1), Loc.tag @@ CRef (f,None)),args@[c,None])
+	CAst.make ~loc:(!@loc) @@ CApp((Some (List.length args+1), CAst.make @@ CRef (f,None)),args@[c,None])
       | c=operconstr; ".("; "@"; f=global;
         args=LIST0 (operconstr LEVEL "9"); ")" ->
-        Loc.tag ~loc:(!@loc) @@ CAppExpl((Some (List.length args+1),f,None),args@[c])
-      | c=operconstr; "%"; key=IDENT -> Loc.tag ~loc:(!@loc) @@ CDelimiters (key,c) ]
+        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) ]
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
       | "("; c = operconstr LEVEL "200"; ")" ->
-          (match snd c with
+          (match c.CAst.v with
               CPrim (Numeral z) when Bigint.is_pos_or_zero z ->
-                Loc.tag ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
+                CAst.make ~loc:(!@loc) @@ CNotation("( _ )",([c],[],[]))
             | _ -> c)
       | "{|"; c = record_declaration; "|}" -> c
       | "`{"; c = operconstr LEVEL "200"; "}" ->
-	  Loc.tag ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
+	  CAst.make ~loc:(!@loc) @@ CGeneralization (Implicit, None, c)
       | "`("; c = operconstr LEVEL "200"; ")" ->
-	  Loc.tag ~loc:(!@loc) @@ CGeneralization (Explicit, None, c)
+	  CAst.make ~loc:(!@loc) @@ CGeneralization (Explicit, None, c)
       ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields -> Loc.tag ~loc:(!@loc) @@ CRecord fs ] ]
+    [ [ fs = record_fields -> CAst.make ~loc:(!@loc) @@ CRecord fs ] ]
   ;
 
   record_fields:
@@ -236,40 +236,40 @@ GEXTEND Gram
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let ty,c1 = match ty, c1 with
-          | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+          | (_,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
-          Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
+          CAst.make ~loc:!@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 (li,id) = match snd fixp with
+          let (li,id) = match fixp.CAst.v with
               CFix(id,_) -> id
             | CCoFix(id,_) -> id
             | _ -> assert false in
-          Loc.tag ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c)
+          CAst.make ~loc:!@loc @@ CLetIn((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" ->
-          Loc.tag ~loc:!@loc @@ CLetTuple (lb,po,c1,c2)
+          CAst.make ~loc:!@loc @@ CLetTuple (lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@
+	    CAst.make ~loc:!@loc @@
             CCases (LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@
+	    CAst.make ~loc:!@loc @@
             CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
 
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@
+	    CAst.make ~loc:!@loc @@
             CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
-          Loc.tag ~loc:(!@loc) @@ CIf (c, po, b1, b2)
+          CAst.make ~loc:(!@loc) @@ CIf (c, po, b1, b2)
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
@@ -278,14 +278,14 @@ GEXTEND Gram
       | c=operconstr LEVEL "9" -> (c,None) ] ]
   ;
   atomic_constr:
-    [ [ g=global; i=instance -> Loc.tag ~loc:!@loc @@ CRef (g,i)
-      | s=sort   -> Loc.tag ~loc:!@loc @@  CSort s
-      | n=INT    -> Loc.tag ~loc:!@loc @@ CPrim (Numeral (Bigint.of_string n))
-      | s=string -> Loc.tag ~loc:!@loc @@ CPrim (String s)
-      | "_"      -> Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None)
-      | "?"; "["; id=ident; "]"  -> Loc.tag ~loc:!@loc @@  CHole (None, IntroIdentifier id, None)
-      | "?"; "["; id=pattern_ident; "]"  -> Loc.tag ~loc:!@loc @@  CHole (None, IntroFresh id, None)
-      | id=pattern_ident; inst = evar_instance -> Loc.tag ~loc:!@loc @@ CEvar(id,inst) ] ]
+    [ [ 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 (Bigint.of_string n))
+      | 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) ] ]
   ;
   inst:
     [ [ id = ident; ":="; c = lconstr -> (id,c) ] ]
@@ -326,7 +326,7 @@ GEXTEND Gram
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
-        br=branches; "end" -> Loc.tag ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ]
+        br=branches; "end" -> CAst.make ~loc:!@loc @@ CCases(RegularStyle,ty,ci,br) ] ]
   ;
   case_item:
     [ [ c=operconstr LEVEL "100";
@@ -368,46 +368,46 @@ GEXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> Loc.tag ~loc:!@loc @@ CPatOr (p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
-        Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ]
+        CAst.make ~loc:!@loc @@ CPatAlias (p, id) ]
     | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
-        (match p with
-	  | _,   CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
-	  | loc, CPatCstr (r, None, l2) ->
+        (let open CAst in match p with
+	  | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp)
+	  | { v = CPatCstr (r, None, l2); loc } ->
                  CErrors.user_err ?loc ~hdr:"compound_pattern"
                  (Pp.str "Nested applications not supported.")
-	  | _,   CPatCstr (r, l1, l2)   -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
-	  | _,   CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp)
+	  | { v = CPatCstr (r, l1, l2) }  -> CAst.make ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
+	  | { v = CPatNotation (n, s, l) } -> CAst.make ~loc:!@loc @@ CPatNotation (n , s, l@lp)
           | _ -> CErrors.user_err
                  ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
                  (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
-        Loc.tag ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
+        CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> Loc.tag ~loc:!@loc @@ CPatDelimiters (key,c) ]
+      [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ]
     | "0"
-      [ r = Prim.reference                -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
-      | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
-      | "_" -> Loc.tag ~loc:!@loc @@ CPatAtom None
+      [ 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
       | "("; p = pattern LEVEL "200"; ")" ->
-          (match p with
-            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
-                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
+          (match p.CAst.v with
+            | CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+                 CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p)
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           let p =
             match p with
-            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
-                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
+            | { CAst.v = CPatPrim (Numeral z) } when Bigint.is_pos_or_zero z ->
+                 CAst.make ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
-	  Loc.tag ~loc:!@loc @@ CPatCast (p, ty)
-      | n = INT    -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
-      | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ]
+	  CAst.make ~loc:!@loc @@ CPatCast (p, ty)
+      | n = INT    -> CAst.make ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+      | s = string -> CAst.make ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
   impl_ident_tail:
     [ [ "}" -> binder_of_name Implicit
@@ -415,7 +415,7 @@ GEXTEND Gram
         (fun na -> CLocalAssum (na::nal,Default Implicit,c))
     | nal=LIST1 name; "}" ->
         (fun na -> CLocalAssum (na::nal,Default Implicit,
-                                Loc.tag ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+                                CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
     | ":"; c=lconstr; "}" ->
 	(fun na -> CLocalAssum ([na],Default Implicit,c))
     ] ]
@@ -449,7 +449,7 @@ GEXTEND Gram
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
           [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2],
-	                  Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
+	                  Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
     ] ]
@@ -458,7 +458,7 @@ GEXTEND Gram
     [ [ l = LIST0 binder -> List.flatten l ] ]
   ;
   binder:
-    [ [ id = name -> [CLocalAssum ([id],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
+    [ [ id = name -> [CLocalAssum ([id],Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
       | bl = closed_binder -> bl ] ]
   ;
   closed_binder:
@@ -467,27 +467,27 @@ GEXTEND Gram
       | "("; id=name; ":"; c=lconstr; ")" ->
           [CLocalAssum ([id],Default Explicit,c)]
       | "("; id=name; ":="; c=lconstr; ")" ->
-          (match c with
-          | (_, CCast(c, CastConv t)) -> [CLocalDef (id,c,Some t)]
+          (match c.CAst.v with
+          | CCast(c, CastConv t) -> [CLocalDef (id,c,Some t)]
           | _ -> [CLocalDef (id,c,None)])
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
           [CLocalDef (id,c,Some t)]
       | "{"; id=name; "}" ->
-          [CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
+          [CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
           [CLocalAssum (id::idl,Default Implicit,c)]
       | "{"; id=name; ":"; c=lconstr; "}" ->
           [CLocalAssum ([id],Default Implicit,c)]
       | "{"; id=name; idl=LIST1 name; "}" ->
-          List.map (fun id -> CLocalAssum ([id],Default Implicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))) (id::idl)
+          List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc:!@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
       | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
 	  List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
       | "'"; p = pattern LEVEL "0" ->
           let (p, ty) =
-            match p with
-            | _, CPatCast (p, ty) -> (p, Some ty)
+            match p.CAst.v with
+            | CPatCast (p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
           [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 488995201..ee0f06fe0 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -120,7 +120,7 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> Loc.tag ~loc:!@loc @@ CCast(c,CastConv t) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ]
   ;
   mode:
     [ [ l = LIST1 [ "+" -> ModeInput
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c8101875d..27f879154 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -233,14 +233,14 @@ GEXTEND Gram
 	DefineBody ([], red, c, None)
       else
         (match c with
-        | _, CCast(c, CastConv t) -> DefineBody (bl, red, c, Some t)
+        | { CAst.v = CCast(c, CastConv t) } -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
         let ((bl, c), tyo) =
           if List.exists (function CLocalPattern _ -> true | _ -> false) bl
           then
             (* FIXME: "red" will be applied to types in bl and Cast with remain *)
-            let c = Loc.tag ~loc:!@loc @@ CCast (c, CastConv t) in
+            let c = CAst.make ~loc:!@loc @@ CCast (c, CastConv t) in
             (([],mkCLambdaN ~loc:!@loc bl c), None)
           else ((bl, c), Some t)
         in
@@ -305,7 +305,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
+      | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -354,14 +354,14 @@ GEXTEND Gram
          t = lconstr; ":="; b = lconstr -> fun id ->
 	   (oc,DefExpr (id,mkCLambdaN ~loc:!@loc l b,Some (mkCProdN ~loc:!@loc l t)))
       | l = binders; ":="; b = lconstr -> fun id ->
-         match snd b with
+         match b.CAst.v with
 	 | CCast(b', (CastConv t|CastVM t|CastNative t)) ->
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b',Some (mkCProdN ~loc:!@loc l t)))
          | _ ->
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id, Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
+    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -380,7 +380,7 @@ GEXTEND Gram
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (Loc.tag ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
 	 -> t l
      ]]
 ;