[location] [ast] Port module AST to CAst

19 files changed, 275 insertions, 265 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 938fe5237..7f2b21e79 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -345,10 +345,10 @@ let raw_push_named (na,raw_value,raw_typ) env =
 
 
 let add_pat_variables pat typ env : Environ.env =
-  let rec add_pat_variables env (loc, pat) typ  : Environ.env =
+  let rec add_pat_variables env pat typ  : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
-    match pat with
+    match pat.CAst.v with
       | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
@@ -398,7 +398,7 @@ let add_pat_variables pat typ env : Environ.env =
 
 
 
-let rec pattern_to_term_and_type env typ  = Loc.with_unloc (function
+let rec pattern_to_term_and_type env typ  = CAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar (Name id) ->
 	mkGVar id
@@ -466,11 +466,12 @@ let rec pattern_to_term_and_type env typ  = Loc.with_unloc (function
 
 let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr rt);
-  match rt with
-    | _, GRef _ | _, GVar _ | _, GEvar _ | _, GPatVar _     | _, GSort _  | _, GHole _  ->
+  let open CAst in
+  match rt.v with
+    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
-    | _, GApp(_,_) ->
+    | GApp(_,_) ->
 	let f,args = glob_decompose_app rt in
 	let args_res : (glob_constr list) build_entry_return =
 	  List.fold_right (* create the arguments lists of constructors and combine them *)
@@ -482,14 +483,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	    (mk_result [] [] avoid)
 	in
 	begin
-	  match Loc.obj f with
+	  match f.v with
 	    | GLambda _  -> 
 		let rec aux t l = 
 		  match l with 
 		    | [] -> t
-		    | u::l -> Loc.tag @@
-			match t with 
-			  | loc, GLambda(na,_,nat,b) -> 
+		    | u::l -> CAst.make @@
+			match t.v with 
+			  | GLambda(na,_,nat,b) -> 
 			      GLetIn(na,u,None,aux b l)
 			  | _ -> 
 			      GApp(t,l)
@@ -550,7 +551,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (Loc.tag @@ GVar id)
+			    (CAst.make @@ GVar id)
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -579,7 +580,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	    | GProd _ -> error "Cannot apply a type"
 	end (* end of the application treatement *)
 
-    | _, GLambda(n,_,t,b) ->
+    | GLambda(n,_,t,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the type
@@ -594,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	let new_env = raw_push_named (new_n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_lam new_n) t_res b_res
-    | _, GProd(n,_,t,b) ->
+    | GProd(n,_,t,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the type
@@ -604,13 +605,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	let new_env = raw_push_named (n,None,t) env in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_prod n) t_res b_res
-    | loc, GLetIn(n,v,typ,b) ->
+    | GLetIn(n,v,typ,b) ->
 	(* we first compute the list of constructor
 	   corresponding to the body of the function,
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
-        let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
+        let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -622,13 +623,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	in
 	let b_res = build_entry_lc new_env funnames avoid b in
 	combine_results (combine_letin n) v_res b_res
-    | _, GCases(_,_,el,brl) ->
+    | GCases(_,_,el,brl) ->
 	(* we create the discrimination function
 	   and treat the case itself
 	*)
 	let make_discr = make_discr_match brl in
 	build_entry_lc_from_case env funnames make_discr el brl avoid
-    | _, GIf(b,(na,e_option),lhs,rhs) ->
+    | GIf(b,(na,e_option),lhs,rhs) ->
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
 	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in
 	let (ind,_) =
@@ -651,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	in
 	(* 		Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
 	build_entry_lc env funnames avoid match_expr
-    | _, GLetTuple(nal,_,b,e) ->
+    | GLetTuple(nal,_,b,e) ->
 	begin
 	  let nal_as_glob_constr =
 	    List.map
@@ -677,8 +678,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  build_entry_lc env funnames avoid match_expr
 
 	end
-    | _, GRec _ -> error "Not handled GRec"
-    | _, GCast(b,_) ->
+    | GRec _ -> error "Not handled GRec"
+    | GCast(b,_) ->
 	build_entry_lc env funnames  avoid b
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
@@ -860,8 +861,8 @@ let is_res id =
 
 
 
-let same_raw_term (_,rt1) (_,rt2) = 
-  match rt1,rt2 with 
+let same_raw_term rt1 rt2 = 
+  match CAst.(rt1.v, rt2.v) with 
     | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
@@ -894,16 +895,17 @@ exception Continue
 let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   observe (str "rebuilding : " ++ pr_glob_constr rt);
   let open Context.Rel.Declaration in
-  match rt with
-    | _, GProd(n,k,t,b) ->
+  let open CAst in
+  match rt.v with
+    | GProd(n,k,t,b) ->
 	let not_free_in_t id = not (is_free_in id t) in
 	let new_crossed_types = t::crossed_types in
 	begin
 	  match t with
-	    | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id ->
+	    | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id ->
 		begin
 		  match args' with
-		    | (_, (GVar this_relname))::args' ->
+		    | { v = GVar this_relname }::args' ->
 			(*i The next call to mk_rel_id is
 			  valid since we are constructing the graph
 			  Ensures by: obvious
@@ -925,7 +927,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt])
+	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) }
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
 		begin
@@ -962,8 +964,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let params,arg' =
 		      ((Util.List.chop nparam args'))
 		    in
-		    let rt_typ = Loc.tag @@
-		       GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None),
+		    let rt_typ = CAst.make @@
+		       GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 env (Evd.from_env env)
@@ -973,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt])
+		      CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
@@ -1042,7 +1044,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     mkGProd(n,t,new_b),id_to_exclude
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
-	    | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2])
+	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) }
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
@@ -1093,7 +1095,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			(Id.Set.filter not_free_in_t id_to_exclude)
 		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	end
-    | _, GLambda(n,k,t,b) ->
+    | GLambda(n,k,t,b) ->
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
@@ -1112,14 +1114,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		then
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  Loc.tag @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+		  CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly (Pp.str "Should not have an anonymous function here")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
-    | loc, GLetIn(n,v,t,b) ->
+    | GLetIn(n,v,t,b) ->
 	begin
-          let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
+          let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1135,10 +1137,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> Loc.tag @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+	    | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
-    | _, GLetTuple(nal,(na,rto),t,b) ->
+    | GLetTuple(nal,(na,rto),t,b) ->
 	assert (Option.is_empty rto);
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
@@ -1161,7 +1163,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
 (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  Loc.tag @@ GLetTuple(nal,(na,None),t,new_b),
+	  CAst.make @@ GLetTuple(nal,(na,None),t,new_b),
 		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
@@ -1187,9 +1189,9 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
-let rec compute_cst_params relnames params gt = Loc.with_unloc (function
+let rec compute_cst_params relnames params gt = CAst.with_val (function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames ->
+  | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
   | GApp(f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
@@ -1211,7 +1213,7 @@ let rec compute_cst_params relnames params gt = Loc.with_unloc (function
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,None) as param)::params',(_, GVar id')::rtl'
+    | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl'
 	when Id.compare id id' == 0 ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 66b9897d0..5abcb100f 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,16 +10,16 @@ open Misctypes
    Some basic functions to rebuild glob_constr
    In each of them the location is Loc.ghost
 *)
-let mkGRef ref          = Loc.tag @@ GRef(ref,None)
-let mkGVar id           = Loc.tag @@ GVar(id)
-let mkGApp(rt,rtl)      = Loc.tag @@ GApp(rt,rtl)
-let mkGLambda(n,t,b)    = Loc.tag @@ GLambda(n,Explicit,t,b)
-let mkGProd(n,t,b)      = Loc.tag @@ GProd(n,Explicit,t,b)
-let mkGLetIn(n,b,t,c)   = Loc.tag @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = Loc.tag @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGSort s           = Loc.tag @@ GSort(s)
-let mkGHole ()          = Loc.tag @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t)        = Loc.tag @@ GCast(b,CastConv t)
+let mkGRef ref          = CAst.make @@ GRef(ref,None)
+let mkGVar id           = CAst.make @@ GVar(id)
+let mkGApp(rt,rtl)      = CAst.make @@ GApp(rt,rtl)
+let mkGLambda(n,t,b)    = CAst.make @@ GLambda(n,Explicit,t,b)
+let mkGProd(n,t,b)      = CAst.make @@ GProd(n,Explicit,t,b)
+let mkGLetIn(n,b,t,c)   = CAst.make @@ GLetIn(n,b,t,c)
+let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
+let mkGSort s           = CAst.make @@ GSort(s)
+let mkGHole ()          = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGCast(b,t)        = CAst.make @@ GCast(b,CastConv t)
 
 (*
   Some basic functions to decompose glob_constrs
@@ -27,7 +27,7 @@ let mkGCast(b,t)        = Loc.tag @@ GCast(b,CastConv t)
 *)
 let glob_decompose_prod =
   let rec glob_decompose_prod args = function
-  | _, GProd(n,k,t,b) ->
+  | { CAst.v = GProd(n,k,t,b) } ->
       glob_decompose_prod ((n,t)::args) b
   | rt -> args,rt
   in
@@ -35,9 +35,9 @@ let glob_decompose_prod =
 
 let glob_decompose_prod_or_letin =
   let rec glob_decompose_prod args = function
-  | _, GProd(n,k,t,b) ->
+  | { CAst.v = GProd(n,k,t,b) } ->
       glob_decompose_prod ((n,None,Some t)::args) b
-  | _, GLetIn(n,b,t,c) ->
+  | { CAst.v = GLetIn(n,b,t,c) } ->
       glob_decompose_prod ((n,Some b,t)::args) c
   | rt -> args,rt
   in
@@ -59,7 +59,7 @@ let glob_decompose_prod_n n =
     if i<=0 then args,c
     else
       match c with
-	| _, GProd(n,_,t,b) ->
+	| { CAst.v = GProd(n,_,t,b) } ->
 	    glob_decompose_prod (i-1) ((n,t)::args) b
 	| rt -> args,rt
   in
@@ -71,9 +71,9 @@ let glob_decompose_prod_or_letin_n n =
     if i<=0 then args,c
     else
       match c with
-	| _, GProd(n,_,t,b) ->
+	| { CAst.v = GProd(n,_,t,b) } ->
 	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| _, GLetIn(n,b,t,c) ->
+	| { CAst.v = GLetIn(n,b,t,c) } ->
 	    glob_decompose_prod (i-1) ((n,Some b,t)::args) c
 	| rt -> args,rt
   in
@@ -84,7 +84,7 @@ let glob_decompose_app =
   let rec decompose_rapp acc rt =
 (*     msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
     match rt with
-    | _, GApp(rt,rtl) ->
+    | { CAst.v = GApp(rt,rtl) } ->
 	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
     | rt -> rt,List.rev acc
   in
@@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na =
 
 let change_vars =
   let rec change_vars mapping rt =
-    Loc.map (function
+    CAst.map (function
       | GRef _ as x -> x
       | GVar id ->
 	  let new_id =
@@ -189,18 +189,19 @@ let change_vars =
 
 
 
-let rec alpha_pat excluded (loc, pat) =
-  match pat with
+let rec alpha_pat excluded pat =
+  let loc = pat.CAst.loc in
+  match pat.CAst.v with
     | PatVar Anonymous ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	(Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+	(CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
     | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
-	  (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),
+	  (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
-	else (Loc.tag ?loc pat),excluded,Id.Map.empty
+	else pat, excluded,Id.Map.empty
     | PatCstr(constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
@@ -218,7 +219,7 @@ let rec alpha_pat excluded (loc, pat) =
 	    ([],new_excluded,map)
 	    patl
 	in
-        (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
+        (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
 
 let alpha_patl excluded patl  =
   let patl,new_excluded,map =
@@ -236,8 +237,8 @@ let alpha_patl excluded patl  =
 
 
 let raw_get_pattern_id pat acc =
-  let rec get_pattern_id (loc, pat) =
-    match pat with
+  let rec get_pattern_id pat =
+    match pat.CAst.v with
       | PatVar(Anonymous) -> assert false
       | PatVar(Name id) ->
 	  [id]
@@ -254,10 +255,11 @@ let raw_get_pattern_id pat acc =
 
 let get_pattern_id pat = raw_get_pattern_id pat []
 
-let rec alpha_rt excluded (loc, rt) =
-  let new_rt = Loc.tag ?loc @@
-    match rt with
-      | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
+let rec alpha_rt excluded rt =
+  let loc = rt.CAst.loc in
+  let new_rt = CAst.make ?loc @@
+    match rt.CAst.v with
+      | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
       | GLambda(Anonymous,k,t,b) ->
 	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
@@ -351,8 +353,8 @@ let rec alpha_rt excluded (loc, rt) =
 	    alpha_rt excluded rhs
 	   )
     | GRec _ -> error "Not handled GRec"
-    | GSort _ -> rt
-    | GHole _ -> rt
+    | GSort _
+    | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
 	      Miscops.map_cast_type (alpha_rt excluded) c)
@@ -375,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) =
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
 let is_free_in id =
-  let rec is_free_in (loc, gt) = match gt with
+  let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function
     | GRef _ ->  false
     | GVar id' -> Id.compare id' id == 0
     | GEvar _ -> false
@@ -411,6 +413,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
+    ) x
   and is_free_in_br (_,(ids,_,rt)) =
     (not (Id.List.mem id ids)) && is_free_in rt
   in
@@ -418,7 +421,7 @@ let is_free_in id =
 
 
 
-let rec pattern_to_term pt = Loc.with_unloc (function
+let rec pattern_to_term pt = CAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar(Name id) ->
 	mkGVar id
@@ -445,39 +448,38 @@ let rec pattern_to_term pt = Loc.with_unloc (function
 
 
 let replace_var_by_term x_id term =
-  let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@
-    match rt with
-      | GRef _ -> rt
-      | GVar id when Id.compare id x_id == 0 -> Loc.obj term
-      | GVar _ -> rt
-      | GEvar _ -> rt
-      | GPatVar _ -> rt
+  let rec replace_var_by_pattern x = CAst.map (function
+      | GVar id when Id.compare id x_id == 0 -> term.CAst.v
+      | GRef _
+      | GVar _
+      | GEvar _
+      | GPatVar _ as rt -> rt
       | GApp(rt',rtl) ->
 	  GApp(replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | GLambda(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+      | GLambda(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GLambda(name,k,t,b) ->
 	  GLambda(name,
 		  k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GProd(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+      | GProd(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GProd(name,k,t,b) ->
 	  GProd(  name,
 	          k,
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GLetIn(Name id,_,_,_) when Id.compare id x_id == 0 -> rt
+      | GLetIn(Name id,_,_,_) as rt when Id.compare id x_id == 0 -> rt
       | GLetIn(name,def,typ,b) ->
 	  GLetIn(name,
 		 replace_var_by_pattern def,
 		 Option.map (replace_var_by_pattern) typ,
 		 replace_var_by_pattern b
 		)
-      | GLetTuple(nal,_,_,_)
+      | GLetTuple(nal,_,_,_) as rt
 	  when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal  ->
 	  rt
       | GLetTuple(nal,(na,rto),def,b) ->
@@ -499,11 +501,12 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern rhs
 	     )
       | GRec _ -> raise (UserError(None,str "Not handled GRec"))
-      | GSort _ -> rt
-      | GHole _ -> rt
+      | GSort _
+      | GHole _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
+    ) x
   and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl
     then br
@@ -520,9 +523,10 @@ exception NotUnifiable
 let rec are_unifiable_aux  = function
   | [] -> ()
   | eq::eqs ->
+      let open CAst in
       match eq with
-	 | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs
-	 | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
+	 | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs
+	 | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -542,9 +546,10 @@ let are_unifiable pat1 pat2 =
 let rec eq_cases_pattern_aux  = function
   | [] -> ()
   | eq::eqs ->
+      let open CAst in
       match eq with
-	 | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs
-	 | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
+	 | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs
+	 | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -564,7 +569,7 @@ let eq_cases_pattern pat1 pat2 =
 
 
 let ids_of_pat =
-  let rec ids_of_pat ids = Loc.with_unloc (function
+  let rec ids_of_pat ids = CAst.with_val (function
     | PatVar Anonymous -> ids
     | PatVar(Name id) -> Id.Set.add id ids
     | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl
@@ -578,7 +583,7 @@ let id_of_name = function
 
 (* TODO: finish Rec caes *)
 let ids_of_glob_constr c =
-  let rec ids_of_glob_constr acc (loc, c) =
+  let rec ids_of_glob_constr acc {loc; CAst.v = c} =
     let idof = id_of_name in
     match c with
       | GVar id -> id::acc
@@ -605,12 +610,11 @@ let ids_of_glob_constr c =
 
 
 let zeta_normalize =
-  let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@
-    match rt with
-      | GRef _ -> rt
-      | GVar _ -> rt
-      | GEvar _ -> rt
-      | GPatVar _ -> rt
+  let rec zeta_normalize_term x = CAst.map (function
+      | GRef _
+      | GVar _
+      | GEvar _
+      | GPatVar _ as rt -> rt
       | GApp(rt',rtl) ->
 	  GApp(zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
@@ -628,9 +632,9 @@ let zeta_normalize =
 		zeta_normalize_term b
 		 )
       | GLetIn(Name id,def,typ,b) ->
-	  Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b)
+	  (zeta_normalize_term (replace_var_by_term id def b)).CAst.v
       | GLetIn(Anonymous,def,typ,b) ->
-          Loc.obj @@ zeta_normalize_term b
+          (zeta_normalize_term b).CAst.v
       | GLetTuple(nal,(na,rto),def,b) ->
 	  GLetTuple(nal,
 		    (na,Option.map zeta_normalize_term rto),
@@ -650,11 +654,12 @@ let zeta_normalize =
 	      zeta_normalize_term rhs
 	     )
       | GRec _ -> raise (UserError(None,str "Not handled GRec"))
-      | GSort _ -> rt
-      | GHole _ -> rt
+      | GSort _
+      | GHole _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(zeta_normalize_term b,
                 Miscops.map_cast_type zeta_normalize_term c)
+    ) x
   and zeta_normalize_br (loc,(idl,patl,res)) =
     (loc,(idl,patl,zeta_normalize_term res))
   in
@@ -665,21 +670,19 @@ let zeta_normalize =
 
 let expand_as =
 
-  let rec add_as map (loc, pat) =
+  let rec add_as map ({loc; CAst.v = pat } as rt) =
     match pat with
       | PatVar _ -> map
       | PatCstr(_,patl,Name id) ->
-	  Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl)
+	  Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
-  let rec expand_as map (loc, rt) =
-    Loc.tag ?loc @@
-    match rt with
-      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt
-      | GVar id ->
+  let rec expand_as map = CAst.map (function
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
+      | GVar id as rt ->
 	  begin
 	    try
-	      Loc.obj @@ Id.Map.find id map
+	      (Id.Map.find id map).CAst.v
 	    with Not_found -> rt
 	  end
       | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
@@ -699,6 +702,7 @@ let expand_as =
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
+    )
   and expand_as_br map (loc,(idl,cpl,rt)) =
     (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f4e9aa372..ab83cb15a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -190,7 +190,7 @@ let build_newrecursive l =
 let is_rec names =
   let names = List.fold_right Id.Set.add names Id.Set.empty in
   let check_id id names =  Id.Set.mem id names in
-  let rec lookup names (loc, gt) = match gt with
+  let rec lookup names gt = match gt.CAst.v with
     | GVar(id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GCast(b,_) -> lookup names b
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index de8dc53f1..394b252aa 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -69,7 +69,7 @@ let chop_rlambda_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match Loc.obj rt with
+	match rt.CAst.v with
 	  | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
 	  | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
 	  | _ ->
@@ -83,7 +83,7 @@ let chop_rprod_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match Loc.obj rt with
+	match rt.CAst.v with
 	  | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 5b51a213a..d4865bf5e 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -66,7 +66,7 @@ let string_of_name = id_of_name %> Id.to_string
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
     match x with
-      | _, GVar x -> Id.equal x f
+      | { CAst.v = GVar x } -> Id.equal x f
       | _ -> false
 
 (** [ident_global_exist id] returns true if identifier [id] is linked
@@ -504,40 +504,40 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
 
 exception NoMerge
 
-let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable =
+let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match c1, c2 with
+  match CAst.(c1.v, c2.v) with
     | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
         let _ = prstr "\nICI1!\n" in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        Loc.tag @@ GApp ((Loc.tag @@ GVar shift.ident) , args)
+        CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args)
     | GApp(f1, arr1), GApp(f2,arr2)  -> raise NoMerge
     | GLetIn(nme,bdy,typ,trm) , _ ->
         let _ = prstr "\nICI2!\n" in
-        let newtrm = merge_app trm (loc2, c2) id1 id2 shift filter_shift_stable in
-        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+        let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
+        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3!\n" in
-        let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in
-        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+        let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
+        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
-let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable =
+let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match c1 , c2 with
+  match CAst.(c1.v, c2.v) with
     | GApp(f1, arr1), GApp(f2,arr2) ->
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        Loc.tag @@ GApp (Loc.tag @@ GVar shift.ident, args)
+        CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args)
           (* FIXME: what if the function appears in the body of the let? *)
     | GLetIn(nme,bdy,typ,trm) , _ ->
       let _ = prstr "\nICI2 '!\n" in
-        let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in
-        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+        let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
+        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3 '!\n" in
-        let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in
-        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+        let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
+        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
@@ -550,14 +550,14 @@ let rec merge_rec_hyps shift accrec
     filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
   let mergeonehyp t reldecl =
     match reldecl with
-      | (nme,x,Some (_, GApp(i,args) as ind))
+      | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind))
         -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
       | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
       | (nme,None,Some _) -> assert false
       | (nme,None,None) | (nme,Some _,Some _) -> assert false in
   match ltyp with
     | [] -> []
-    | (nme,None,Some (_, GApp(f, largs) as t)) :: lt when isVarf ind2name f ->
+    | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f ->
         let rechyps = List.map (mergeonehyp t) accrec in
         rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
     | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
@@ -573,7 +573,7 @@ let find_app (nme:Id.t) ltyp =
       (List.map
           (fun x ->
             match x with
-              | _,None,Some (_, GApp(f,_)) when isVarf nme f -> raise (Found 0)
+              | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0)
               | _ -> ())
           ltyp);
     false
@@ -632,8 +632,8 @@ let rec merge_types shift accrec1
 
           rechyps , concl
       | (nme,None, Some t1)as e ::lt1 ->
-          (match t1 with
-            | _, GApp(f,carr) when isVarf ind1name f ->
+          (match t1.CAst.v with
+            | GApp(f,carr) when isVarf ind1name f ->
                 merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
             | _ ->
                 let recres, recconcl2 =
@@ -864,7 +864,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
     | LocalAssum (nme,t) ->
         let t = EConstr.of_constr t in
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
-        Loc.tag @@ GProd (nme,Explicit,traw,t2)
+        CAst.make @@ GProd (nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9e469c756..8c8839944 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -188,15 +188,15 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
     in
     let env = Environ.push_rel_context context (Global.env ()) in
     let glob_body =
-      Loc.tag @@
+      CAst.make @@
        GCases
 	(RegularStyle,None,
-	 [Loc.tag @@ GApp(Loc.tag @@ GRef(fterm,None), List.rev_map (fun x_id -> Loc.tag @@ GVar x_id) rev_x_id_l),
+	 [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l),
 	  (Anonymous,None)],
-	 [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
-			   [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous],
+	 [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+			   [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous],
                            Anonymous)],
-	    Loc.tag @@ GVar v_id)])
+	    CAst.make @@ GVar v_id)])
     in
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index dc43930e4..9d50b6e6f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -631,14 +631,14 @@ let subst_var_with_hole occ tid t =
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec = function
-    | (_, GVar id) as x -> 
+    | { CAst.v = GVar id } as x -> 
         if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
            else
 	     (incr locref;
-              Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+              CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
                      Misctypes.IntroAnonymous, None)))
         else x
@@ -651,12 +651,12 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | _, GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
-           Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+           CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 1f40c67b5..b4a0e46ae 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with (_, GVar id') when Id.equal id' id -> true | _ -> false in
+  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in
     Tacticals.onAllHypsAndConcl
       (fun cl ->
         match cl with
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 58473d7dd..87b79374e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1085,7 +1085,7 @@ type 'a extra_genarg_printer =
   let strip_prod_binders_glob_constr n (ty,_) =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
-        match Loc.obj ty with
+        match ty.CAst.v with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
           | _ -> error "Cannot translate fix tactic: not enough products" in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 566dd8ed7..8751a14c7 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -108,12 +108,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None))
+      (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+      (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      Loc.tag @@ GRef (locate_global_with_alias lqid,None), 
+      CAst.make @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (CAst.make @@ CRef (r,None))
 
 let intern_move_location ist = function
@@ -272,7 +272,7 @@ let intern_destruction_arg ist = function
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
 	match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
-	| (loc, GVar id), _ -> clear,ElimOnIdent (loc,id)
+	| {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
 	clear,ElimOnIdent (loc,id)
@@ -350,7 +350,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
       let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
       let c = Constrintern.interp_reference sign r in
-      match Loc.obj c with
+      match c.CAst.v with
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 449027b52..91bc46fe7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -697,7 +697,7 @@ let interp_typed_pattern ist env sigma (_,c,_) =
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
-    | (_, GVar id), _ ->
+    | { CAst.v = GVar id }, _ ->
       let v = Id.Map.find id ist.lfun in
       sigma, List.map inj_fun (coerce_to_constr_list env v)
     | _ ->
@@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (Loc.tag ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+          let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e2a6ad55c..2b64204c9 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -131,7 +131,7 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.tag (tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (Loc.tag @@ GVar(Id.of_string"t"),None));
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None));
    TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c11c9f83b..9a0dfbf1c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -158,10 +158,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
-let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None)
-let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args)
-let mkRCast rc rt =  Loc.tag @@ GCast (rc, dC rt)
-let mkRLambda n s t = Loc.tag @@ GLambda (n, Explicit, s, t)
+let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None)
+let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
+let mkRCast rc rt =  CAst.make @@ GCast (rc, dC rt)
+let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
 
 (* ssrterm conbinators *)
 let combineCG t1 t2 f g = match t1, t2 with
@@ -1022,7 +1022,7 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 let id_of_cpattern = let open CAst in function
   | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x
   | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x
-  | _,((_, GRef (VarRef x, _)) ,None) -> Some x
+  | _,({ v = GRef (VarRef x, _)} ,None) -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
@@ -1121,9 +1121,10 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   let eAsXInT e x t = E_As_X_In_T(e,x,t) in
   let mkG ?(k=' ') x = k,(x,None) in
   let decode ist t ?reccall f g =
+    let open CAst in
     try match (pf_intern_term ist gl t) with
-    | _, GCast((_, GHole _),CastConv((_, GLambda(Name x,_,_,c)))) -> f x (' ',(c,None))
-    | _, GVar id
+    | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None))
+    | { v = GVar id }
       when Id.Map.mem id ist.lfun &&
            not(Option.is_empty reccall) &&
            not(Option.is_empty wit_ssrpatternarg) ->
@@ -1164,18 +1165,18 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         thin name sigma e)
       sigma new_evars in
     sigma in
-  let red = let rec decode_red (ist,red) = match red with
-    | T(k,((_, GCast ((_, GHole _),CastConv((_, GLambda (Name id,_,_,t))))),None))
+  let red = let rec decode_red (ist,red) = let open CAst in match red with
+    | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None))
         when let id = string_of_id id in let len = String.length id in
         (len > 8 && String.sub id 0 8 = "_ssrpat_") ->
         let id = string_of_id id in let len = String.length id in
         (match String.sub id 8 (len - 8), t with
-        | "In", (_, GApp( _, [t])) -> decodeG t xInT (fun x -> T x)
-        | "In", (_, GApp( _, [e; t])) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
-        | "In", (_, GApp( _, [e; t; e_in_t])) ->
+        | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x)
+        | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id)
+        | "In", { v = GApp( _, [e; t; e_in_t]) } ->
             decodeG t (eInXInT (mkG e))
               (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", (_, GApp(_, [e; t])) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
+        | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
         | _ -> bad_enc id ())
     | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x)
     | In_T t -> decode ist t inXInT inT
@@ -1201,7 +1202,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ?loc) b))
-  | None -> a,(Loc.tag ?loc @@ GLetIn (x, Loc.tag ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
+  | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
@@ -1374,10 +1375,10 @@ let pf_fill_occ_term gl occ t =
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
-let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef  id, None), None)
+let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef  id, None), None)
 
 let is_wildcard : cpattern -> bool = function
-  | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true
+  | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true
   | _ -> false
 
 (* "ssrpattern" *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index ed977c416..e7eea0284 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -41,9 +41,9 @@ let interp_ascii ?loc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     (Loc.tag ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
+     (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
      :: (aux (n-1) (p/2)) in
-  Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
+  CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string ?loc s =
   let p =
@@ -59,12 +59,12 @@ let interp_ascii_string ?loc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when Int.equal n 0 -> 0
-    | (_, GRef (k,_))::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | (_, GRef (k,_))::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
     let aux = function
-    | _, GApp ((_, GRef (k,_)),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -80,4 +80,4 @@ let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([Loc.tag @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+    ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 5cdd82024..9a4cd6c25 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -36,11 +36,11 @@ let warn_large_nat =
 let nat_of_int ?loc n =
   if is_pos_or_zero n then begin
       if less_than threshold n then warn_large_nat ();
-      let ref_O = Loc.tag ?loc @@ GRef (glob_O, None) in
-      let ref_S = Loc.tag ?loc @@ GRef (glob_S, None) in
+      let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in
+      let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in
       let rec mk_nat acc n =
 	if n <> zero then
-	  mk_nat (Loc.tag ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
+	  mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -55,8 +55,8 @@ let nat_of_int ?loc n =
 
 exception Non_closed_number
 
-let rec int_of_nat x = Loc.with_unloc (function
-  | GApp ((_, GRef (s,_)),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+let rec int_of_nat x = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
   | GRef (z,_) when Globnames.eq_gr z glob_O -> zero
   | _ -> raise Non_closed_number
   ) x
@@ -74,4 +74,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,datatypes_module_name)
     nat_of_int
-    ([Loc.tag @@ GRef (glob_S,None); Loc.tag @@ GRef (glob_O,None)], uninterp_nat, true)
+    ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 3ee64ba7e..e23852bf8 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -87,9 +87,9 @@ exception Non_closed
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
 let int31_of_pos_bigint ?loc n =
-  let ref_construct = Loc.tag ?loc @@ GRef (int31_construct, None) in
-  let ref_0 = Loc.tag ?loc @@ GRef (int31_0, None) in
-  let ref_1 = Loc.tag ?loc @@ GRef (int31_1, None) in
+  let ref_construct = CAst.make ?loc @@ GRef (int31_construct, None) in
+  let ref_0 = CAst.make ?loc @@ GRef (int31_0, None) in
+  let ref_1 = CAst.make ?loc @@ GRef (int31_1, None) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -97,7 +97,7 @@ let int31_of_pos_bigint ?loc n =
       let (q,r) = div2_with_rest n in
 	(if r then ref_1 else ref_0)::(args (counter-1) q)
   in
-  Loc.tag ?loc @@ GApp (ref_construct, List.rev (args 31 n))
+  CAst.make ?loc @@ GApp (ref_construct, List.rev (args 31 n))
 
 let error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
@@ -114,12 +114,12 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | (_, GRef (b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
-      | (_, GRef (b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
+      | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
+      | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
   function
-  | _, GApp ((_, GRef (c, _)), args) when eq_gr c int31_construct -> args_parsing args zero
+  | { CAst.v = GApp ({ CAst.v = GRef (c, _)}, args) } when eq_gr c int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
 let uninterp_int31 i =
@@ -132,7 +132,7 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([Loc.tag @@ GRef (int31_construct, None)],
+  ([CAst.make @@ GRef (int31_construct, None)],
    uninterp_int31,
    true)
 
@@ -163,16 +163,16 @@ let height bi =
 
 (* n must be a non-negative integer (from bigint.ml) *)
 let word_of_pos_bigint ?loc hght n =
-  let ref_W0 = Loc.tag ?loc @@ GRef (zn2z_W0, None) in
-  let ref_WW = Loc.tag ?loc @@ GRef (zn2z_WW, None) in
+  let ref_W0 = CAst.make ?loc @@ GRef (zn2z_W0, None) in
+  let ref_WW = CAst.make ?loc @@ GRef (zn2z_WW, None) in
   let rec decomp hgt n =
     if hgt <= 0 then
       int31_of_pos_bigint ?loc n
     else if equal n zero then
-      Loc.tag ?loc @@ GApp (ref_W0, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
+      CAst.make ?loc @@ GApp (ref_W0, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)])
     else
       let (h,l) = split_at hgt n in
-      Loc.tag ?loc @@ GApp (ref_WW, [Loc.tag ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
+      CAst.make ?loc @@ GApp (ref_WW, [CAst.make ?loc @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None);
 			   decomp (hgt-1) h;
 			   decomp (hgt-1) l])
   in
@@ -180,13 +180,13 @@ let word_of_pos_bigint ?loc hght n =
 
 let bigN_of_pos_bigint ?loc n =
   let h = height n in
-  let ref_constructor = Loc.tag ?loc @@ GRef (bigN_constructor h, None) in
+  let ref_constructor = CAst.make ?loc @@ GRef (bigN_constructor h, None) in
   let word = word_of_pos_bigint ?loc h n in
   let args =
     if h < n_inlined then [word]
     else [Nat_syntax_plugin.Nat_syntax.nat_of_int ?loc (of_int (h-n_inlined));word]
   in
-  Loc.tag ?loc @@ GApp (ref_constructor, args)
+  CAst.make ?loc @@ GApp (ref_constructor, args)
 
 let bigN_error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
@@ -203,14 +203,14 @@ let interp_bigN ?loc n =
 let bigint_of_word =
   let rec get_height rc =
     match rc with
-    | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW ->
+    | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW ->
       1+max (get_height lft) (get_height rght)
     | _ -> 0
   in
   let rec transform hght rc =
     match rc with
-    | _, GApp ((_, GRef(c,_)),_) when eq_gr c zn2z_W0-> zero
-    | _, GApp ((_, GRef(c,_)), [_;lft;rght]) when eq_gr c zn2z_WW->
+    | { CAst.v = GApp ({ CAst.v = GRef(c,_)},_)} when eq_gr c zn2z_W0-> zero
+    | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [_;lft;rght]) } when eq_gr c zn2z_WW->
       let new_hght = hght-1 in
       add (mult (rank new_hght)
              (transform new_hght lft))
@@ -223,8 +223,8 @@ let bigint_of_word =
 
 let bigint_of_bigN rc =
   match rc with
-  | _, GApp (_,[one_arg]) -> bigint_of_word one_arg
-  | _, GApp (_,[_;second_arg]) -> bigint_of_word second_arg
+  | { CAst.v = GApp (_,[one_arg]) } -> bigint_of_word one_arg
+  | { CAst.v = GApp (_,[_;second_arg]) } -> bigint_of_word second_arg
   | _ -> raise Non_closed
 
 let uninterp_bigN rc =
@@ -240,7 +240,7 @@ let uninterp_bigN rc =
 let bigN_list_of_constructors =
   let rec build i =
     if i < n_inlined+1 then
-      (Loc.tag @@ GRef (bigN_constructor i,None))::(build (i+1))
+      (CAst.make @@ GRef (bigN_constructor i,None))::(build (i+1))
     else
       []
   in
@@ -257,17 +257,17 @@ let _ = Notation.declare_numeral_interpreter bigN_scope
 
 (*** Parsing for bigZ in digital notation ***)
 let interp_bigZ ?loc n =
-  let ref_pos = Loc.tag ?loc @@ GRef (bigZ_pos, None) in
-  let ref_neg = Loc.tag ?loc @@ GRef (bigZ_neg, None) in
+  let ref_pos = CAst.make ?loc @@ GRef (bigZ_pos, None) in
+  let ref_neg = CAst.make ?loc @@ GRef (bigZ_neg, None) in
   if is_pos_or_zero n then
-    Loc.tag ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
+    CAst.make ?loc @@ GApp (ref_pos, [bigN_of_pos_bigint ?loc n])
   else
-    Loc.tag ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
+    CAst.make ?loc @@ GApp (ref_neg, [bigN_of_pos_bigint ?loc (neg n)])
 
 (* pretty printing functions for bigZ *)
 let bigint_of_bigZ = function
-  | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
-  | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigZ_neg ->
+  | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_pos -> bigint_of_bigN one_arg
+  | { CAst.v = GApp ({ CAst.v = GRef(c,_) }, [one_arg])} when eq_gr c bigZ_neg ->
       let opp_val = bigint_of_bigN one_arg in
       if equal opp_val zero then
 	raise Non_closed
@@ -286,19 +286,19 @@ let uninterp_bigZ rc =
 let _ = Notation.declare_numeral_interpreter bigZ_scope
   (bigZ_path, bigZ_module)
   interp_bigZ
-  ([Loc.tag @@ GRef (bigZ_pos, None);
-    Loc.tag @@ GRef (bigZ_neg, None)],
+  ([CAst.make @@ GRef (bigZ_pos, None);
+    CAst.make @@ GRef (bigZ_neg, None)],
    uninterp_bigZ,
    true)
 
 (*** Parsing for bigQ in digital notation ***)
 let interp_bigQ ?loc n =
-  let ref_z = Loc.tag ?loc @@ GRef (bigQ_z, None) in
-  Loc.tag ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
+  let ref_z = CAst.make ?loc @@ GRef (bigQ_z, None) in
+  CAst.make ?loc @@ GApp (ref_z, [interp_bigZ ?loc n])
 
 let uninterp_bigQ rc =
   try match rc with
-    | _, GApp ((_, GRef(c,_)), [one_arg]) when eq_gr c bigQ_z ->
+    | { CAst.v = GApp ({ CAst.v = GRef(c,_)}, [one_arg]) } when eq_gr c bigQ_z ->
 	Some (bigint_of_bigZ one_arg)
     | _ -> None (* we don't pretty-print yet fractions *)
   with Non_closed -> None
@@ -307,5 +307,5 @@ let uninterp_bigQ rc =
 let _ = Notation.declare_numeral_interpreter bigQ_scope
   (bigQ_path, bigQ_module)
   interp_bigQ
-  ([Loc.tag @@ GRef (bigQ_z, None)], uninterp_bigQ,
+  ([CAst.make @@ GRef (bigQ_z, None)], uninterp_bigQ,
    true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index b7041d045..7ce066c59 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -42,13 +42,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
-  let ref_xI = Loc.tag @@ GRef (glob_xI, None) in
-  let ref_xH = Loc.tag @@ GRef (glob_xH, None) in
-  let ref_xO = Loc.tag @@ GRef (glob_xO, None) in
+  let ref_xI = CAst.make @@ GRef (glob_xI, None) in
+  let ref_xH = CAst.make @@ GRef (glob_xH, None) in
+  let ref_xO = CAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> Loc.tag @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> Loc.tag @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -58,9 +58,9 @@ let pos_of_bignat ?loc x =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | _, GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -81,18 +81,18 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    Loc.tag @@ GApp(Loc.tag @@ GRef (sgn,None), [pos_of_bignat ?loc n])
+    CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
-    Loc.tag @@ GRef (glob_ZERO, None)
+    CAst.make @@ GRef (glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_z = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -108,14 +108,14 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
 
 let r_of_int ?loc z =
-  Loc.tag @@ GApp (Loc.tag @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+  CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
 let bigint_of_r = function
-  | _, GApp ((_, GRef (o,_)), [a]) when Globnames.eq_gr o glob_IZR ->
+  | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR ->
       bigint_of_z a
   | _ -> raise Non_closed_number
 
@@ -128,6 +128,6 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([Loc.tag @@ GRef (glob_IZR, None)],
+  ([CAst.make @@ GRef (glob_IZR, None)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 49cb9355c..b7f13b040 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -36,8 +36,8 @@ open Lazy
 let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then Loc.tag ?loc @@ GRef (force glob_EmptyString, None) else
-     Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef (force glob_String, None),
+     if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+     CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None),
        [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -45,11 +45,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | _, GApp ((_, GRef (k,_)),[a;s]) when eq_gr k (force glob_String) ->
+    | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | _, GRef (z,_) when eq_gr z (force glob_EmptyString) ->
+    | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +61,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([Loc.tag @@ GRef (static_glob_String,None);
-      Loc.tag @@ GRef (static_glob_EmptyString,None)],
+    ([CAst.make @@ GRef (static_glob_String,None);
+      CAst.make @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 96c1f3e39..479448e06 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x = 
-  let ref_xI = Loc.tag ?loc @@ GRef (glob_xI, None) in
-  let ref_xH = Loc.tag ?loc @@ GRef (glob_xH, None) in
-  let ref_xO = Loc.tag ?loc @@ GRef (glob_xO, None) in
+  let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in
+  let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in
+  let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> Loc.tag ?loc @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> Loc.tag ?loc @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -68,11 +68,12 @@ let interp_positive ?loc n =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-let rec bignat_of_pos = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | _, GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
+let rec bignat_of_pos x = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
+  ) x
 
 let uninterp_positive p =
   try
@@ -87,9 +88,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([Loc.tag @@ GRef (glob_xI, None);
-    Loc.tag @@ GRef (glob_xO, None);
-    Loc.tag @@ GRef (glob_xH, None)],
+  ([CAst.make @@ GRef (glob_xI, None);
+    CAst.make @@ GRef (glob_xO, None);
+    CAst.make @@ GRef (glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -106,9 +107,9 @@ let glob_Npos = ConstructRef path_of_Npos
 
 let n_path = make_path binnums "N"
 
-let n_of_binnat ?loc pos_or_neg n = Loc.tag ?loc @@
+let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@
   if not (Bigint.equal n zero) then
-    GApp(Loc.tag @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
+    GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
   else
     GRef(glob_N0, None)
 
@@ -123,10 +124,11 @@ let n_of_int ?loc n =
 (* Printing N via scopes                                              *)
 (**********************************************************************)
 
-let bignat_of_n = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
-  | _, GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
+let bignat_of_n = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
+  )
 
 let uninterp_n p =
   try Some (bignat_of_n p)
@@ -138,8 +140,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([Loc.tag @@ GRef (glob_N0, None);
-    Loc.tag @@ GRef (glob_Npos, None)],
+  ([CAst.make @@ GRef (glob_N0, None);
+    CAst.make @@ GRef (glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -161,19 +163,20 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    Loc.tag ?loc @@ GApp(Loc.tag ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
+    CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
   else
-    Loc.tag ?loc @@ GRef(glob_ZERO, None)
+    CAst.make ?loc @@ GRef(glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_z = function
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | _, GApp ((_, GRef (b,_)),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | _, GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+let bigint_of_z = CAst.with_val (function
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
+  )
 
 let uninterp_z p =
   try
@@ -186,8 +189,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([Loc.tag @@ GRef (glob_ZERO, None);
-    Loc.tag @@ GRef (glob_POS, None);
-    Loc.tag @@ GRef (glob_NEG, None)],
+  ([CAst.make @@ GRef (glob_ZERO, None);
+    CAst.make @@ GRef (glob_POS, None);
+    CAst.make @@ GRef (glob_NEG, None)],
   uninterp_z,
   true)