[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, 13 insertions, 13 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index fb300dbc1..f9a3b01b6 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -147,14 +147,14 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	  (fun avoid (clname, _) ->
 	    match clname with
 	    | Some (cl, b) ->
-		let t = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None) in
+		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
     | Explicit -> cl, Id.Set.empty
   in
   let tclass = 
-    if generalize then Loc.tag @@ CGeneralization (Implicit, Some AbsPi, tclass) 
+    if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) 
     else tclass 
   in
   let k, u, cty, ctx', ctx, len, imps, subst =
@@ -217,7 +217,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     else (
       let props =
 	match props with
-	| Some (true, (_loc, CRecord fs)) ->
+	| Some (true, { CAst.v = CRecord fs }) ->
 	    if List.length fs > List.length k.cl_props then
 	      mismatched_props env' (List.map snd fs) k.cl_props;
 	    Some (Inl fs)
@@ -261,7 +261,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       ((Loc.tag @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
+		       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
diff --git a/vernac/command.ml b/vernac/command.ml
index 82d7b19d7..12df344c2 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -53,7 +53,7 @@ let rec under_binders env sigma f n c =
 	  mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
       | _ -> assert false
 
-let rec complete_conclusion a cs = Loc.map_with_loc (fun ?loc -> function
+let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
   | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
   | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
   | CHole (k, _, _) ->
@@ -62,7 +62,7 @@ let rec complete_conclusion a cs = Loc.map_with_loc (fun ?loc -> function
 	user_err ?loc
 	 (strbrk"Cannot infer the non constant arguments of the conclusion of "
 	  ++ pr_id cs ++ str ".");
-      let args = List.map (fun id -> Loc.tag ?loc @@ CRef(Ident(loc,id),None)) params in
+      let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in
       CAppExpl ((None,Ident(loc,name),None),List.rev args)
   | c -> c
   )
@@ -683,7 +683,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun (((_,indname),pl),_,ar,lc) -> {
     ind_name = indname; ind_univs = pl;
-    ind_arity = Option.cata (fun x -> x) (Loc.tag @@ CSort (GType [])) ar;
+    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
@@ -1354,7 +1354,7 @@ let do_program_fixpoint local poly l =
 	     
     | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
 	build_wellfounded (id, pl, n, bl, typ, out_def def) poly
-	  (Option.default (Loc.tag @@ CRef (lt_ref,None)) r) m ntn
+	  (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
 	  
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
 	let fixl,ntns = extract_fixpoint_components true l in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index feacfe915..83896992c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = Loc.tag @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
+let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None)
 
 let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
@@ -1477,7 +1477,7 @@ let add_class_scope scope cl =
 (* Check if abbreviation to a name and avoid early insertion of
    maximal implicit arguments *)
 let try_interp_name_alias = function
-  | [], (_loc, CRef (ref,_)) -> intern_reference ref
+  | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
   | _ -> raise Not_found
 
 let add_syntactic_definition ident (vars,c) local onlyparse =
diff --git a/vernac/record.ml b/vernac/record.ml
index 8bd583b81..43a24e167 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -94,7 +94,7 @@ let compute_constructor_level evars env l =
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
   | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c
-                                                       | None   -> Loc.tag ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
+                                                       | None   -> CAst.make ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
 
 let binders_of_decls = List.map binder_of_decl
 
@@ -121,8 +121,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     | Some t -> 
        let env = push_rel_context newps env0 in
        let poly =
-         match snd t with
-         | CSort (Misctypes.GType []) -> true | _ -> false in
+         match t with
+         | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_all env !evars s in
        let s = EConstr.Unsafe.to_constr s in