[location] Switch glob_constr to Loc.located

1 files changed, 157 insertions, 171 deletions

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 51ca8c471..01e607412 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 = GRef(Loc.ghost,ref,None)
-let mkGVar id = GVar(Loc.ghost,id)
-let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl)
-let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b)
-let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b)
-let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c)
-let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl)
-let mkGSort s = GSort(Loc.ghost,s)
-let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t)
+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)
 
 (*
   Some basic functions to decompose glob_constrs
@@ -27,7 +27,7 @@ let mkGCast(b,t) = GCast(Loc.ghost,b,CastConv t)
 *)
 let glob_decompose_prod =
   let rec glob_decompose_prod args = function
-  | GProd(_,n,k,t,b) ->
+  | _, 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) ->
+  | _, GProd(n,k,t,b) ->
       glob_decompose_prod ((n,None,Some t)::args) b
-  | GLetIn(_,n,b,t,c) ->
+  | _, 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) ->
+	| _, 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) ->
+	| _, GProd(n,_,t,b) ->
 	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| GLetIn(_,n,b,t,c) ->
+	| _, 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) ->
+    | _, GApp(rt,rtl) ->
 	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
     | rt -> rt,List.rev acc
   in
@@ -120,75 +120,70 @@ let remove_name_from_mapping mapping na =
 
 let change_vars =
   let rec change_vars mapping rt =
-    match rt with
-      | GRef _ -> rt
-      | GVar(loc,id) ->
+    Loc.map (function
+      | GRef _ as x -> x
+      | GVar id ->
 	  let new_id =
 	    try
 	      Id.Map.find id mapping
 	    with Not_found -> id
 	  in
-	  GVar(loc,new_id)
-      | GEvar _ -> rt
-      | GPatVar _ -> rt
-      | GApp(loc,rt',rtl) ->
-	  GApp(loc,
-	       change_vars mapping rt',
+	  GVar(new_id)
+      | GEvar _ as x   -> x
+      | GPatVar _ as x -> x
+      | GApp(rt',rtl) ->
+	  GApp(change_vars mapping rt',
 	       List.map (change_vars mapping) rtl
 	      )
-      | GLambda(loc,name,k,t,b) ->
-	  GLambda(loc,
-		  name,
+      | GLambda(name,k,t,b) ->
+	  GLambda(name,
 		  k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | GProd(loc,name,k,t,b) ->
-	  GProd(loc,
-		  name,
+      | GProd(name,k,t,b) ->
+	  GProd(  name,
 	          k,
 		  change_vars mapping t,
 		  change_vars (remove_name_from_mapping mapping name) b
 		 )
-      | GLetIn(loc,name,def,typ,b) ->
-	  GLetIn(loc,
-		 name,
+      | GLetIn(name,def,typ,b) ->
+	  GLetIn(name,
 		 change_vars mapping def,
 		 Option.map (change_vars mapping) typ,
 		 change_vars (remove_name_from_mapping mapping name) b
 		)
-      | GLetTuple(loc,nal,(na,rto),b,e) ->
+      | GLetTuple(nal,(na,rto),b,e) ->
 	  let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
-	  GLetTuple(loc,
-		    nal,
+	  GLetTuple(nal,
 		    (na, Option.map (change_vars mapping) rto),
 		    change_vars mapping b,
 		    change_vars new_mapping e
 		   )
-      | GCases(loc,sty,infos,el,brl) ->
-	  GCases(loc,sty,
+      | GCases(sty,infos,el,brl) ->
+	  GCases(sty,
 		 infos,
 		 List.map (fun (e,x) -> (change_vars mapping e,x)) el,
 		 List.map (change_vars_br mapping) brl
 		)
-      | GIf(loc,b,(na,e_option),lhs,rhs) ->
-	  GIf(loc,
-	      change_vars mapping b,
+      | GIf(b,(na,e_option),lhs,rhs) ->
+	  GIf(change_vars mapping b,
 	      (na,Option.map (change_vars mapping) e_option),
 	      change_vars mapping lhs,
 	      change_vars mapping rhs
 	     )
       | GRec _ -> error "Local (co)fixes are not supported"
-      | GSort _ -> rt
-      | GHole _ -> rt
-      | GCast(loc,b,c) ->
-	  GCast(loc,change_vars mapping b,
+      | GSort _ as x -> x
+      | GHole _ as x -> x
+      | GCast(b,c) ->
+	  GCast(change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
-  and change_vars_br mapping ((loc,idl,patl,res) as br) =
+      ) rt
+  and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
     if Id.Map.is_empty new_mapping
     then br
-    else (loc,idl,patl,change_vars new_mapping res)
+    else (loc,(idl,patl,change_vars new_mapping res))
   in
   change_vars
 
@@ -259,30 +254,30 @@ let raw_get_pattern_id pat acc =
 
 let get_pattern_id pat = raw_get_pattern_id pat []
 
-let rec alpha_rt excluded rt =
-  let new_rt =
+let rec alpha_rt excluded (loc, rt) =
+  let new_rt = Loc.tag ~loc @@
     match rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
-      | GLambda(loc,Anonymous,k,t,b) ->
+      | 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
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
-	  GLambda(loc,Name new_id,k,new_t,new_b)
-      | GProd(loc,Anonymous,k,t,b) ->
+	  GLambda(Name new_id,k,new_t,new_b)
+      | GProd(Anonymous,k,t,b) ->
 	let new_t = alpha_rt excluded t in
 	let new_b = alpha_rt excluded b in
-	GProd(loc,Anonymous,k,new_t,new_b)
-    | GLetIn(loc,Anonymous,b,t,c) ->
+	GProd(Anonymous,k,new_t,new_b)
+    | GLetIn(Anonymous,b,t,c) ->
 	let new_b = alpha_rt excluded b in
 	let new_t = Option.map (alpha_rt excluded) t in
 	let new_c = alpha_rt excluded c in
-	GLetIn(loc,Anonymous,new_b,new_t,new_c)
-    | GLambda(loc,Name id,k,t,b) ->
+	GLetIn(Anonymous,new_b,new_t,new_c)
+    | GLambda(Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if Id.equal new_id id
-	  then t,b
+	  then t, b
 	  else
 	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
@@ -290,8 +285,8 @@ let rec alpha_rt excluded rt =
 	let new_excluded = new_id::excluded in
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	GLambda(loc,Name new_id,k,new_t,new_b)
-    | GProd(loc,Name id,k,t,b) ->
+	GLambda(Name new_id,k,new_t,new_b)
+    | GProd(Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let new_excluded = new_id::excluded in
 	let t,b =
@@ -303,8 +298,8 @@ let rec alpha_rt excluded rt =
 	in
 	let new_t = alpha_rt new_excluded t in
 	let new_b = alpha_rt new_excluded b in
-	GProd(loc,Name new_id,k,new_t,new_b)
-    | GLetIn(loc,Name id,b,t,c) ->
+	GProd(Name new_id,k,new_t,new_b)
+    | GLetIn(Name id,b,t,c) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let c =
 	  if Id.equal new_id id then c
@@ -314,10 +309,9 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	let new_t = Option.map (alpha_rt new_excluded) t in
 	let new_c = alpha_rt new_excluded c in
-	GLetIn(loc,Name new_id,new_b,new_t,new_c)
-
+	GLetIn(Name new_id,new_b,new_t,new_c)
 
-    | GLetTuple(loc,nal,(na,rto),t,b) ->
+    | GLetTuple(nal,(na,rto),t,b) ->
 	let rev_new_nal,new_excluded,mapping =
 	  List.fold_left
 	    (fun (nal,excluded,mapping) na ->
@@ -344,14 +338,14 @@ let rec alpha_rt excluded rt =
 	let new_t = alpha_rt new_excluded new_t in
 	let new_b = alpha_rt new_excluded new_b in
 	let new_rto = Option.map (alpha_rt new_excluded) new_rto  in
-	GLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
-    | GCases(loc,sty,infos,el,brl) ->
+	GLetTuple(new_nal,(na,new_rto),new_t,new_b)
+    | GCases(sty,infos,el,brl) ->
 	let new_el =
 	  List.map (function (rt,i) -> alpha_rt excluded rt, i) el
 	in
-	GCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
-    | GIf(loc,b,(na,e_o),lhs,rhs) ->
-	GIf(loc,alpha_rt excluded b,
+	GCases(sty,infos,new_el,List.map (alpha_br excluded) brl)
+    | GIf(b,(na,e_o),lhs,rhs) ->
+	GIf(alpha_rt excluded b,
 	    (na,Option.map (alpha_rt excluded) e_o),
 	    alpha_rt excluded lhs,
 	    alpha_rt excluded rhs
@@ -359,66 +353,65 @@ let rec alpha_rt excluded rt =
     | GRec _ -> error "Not handled GRec"
     | GSort _ -> rt
     | GHole _ -> rt
-    | GCast (loc,b,c) ->
-	GCast(loc,alpha_rt excluded b,
+    | GCast (b,c) ->
+	GCast(alpha_rt excluded b,
 	      Miscops.map_cast_type (alpha_rt excluded) c)
-    | GApp(loc,f,args) ->
-	GApp(loc,
-	     alpha_rt excluded f,
+    | GApp(f,args) ->
+	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
 	    )
   in
   new_rt
 
-and alpha_br excluded (loc,ids,patl,res) =
+and alpha_br excluded (loc,(ids,patl,res)) =
   let new_patl,new_excluded,mapping = alpha_patl excluded patl in
   let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
   let new_excluded = new_ids@excluded in
   let renamed_res = change_vars mapping res in
   let new_res = alpha_rt new_excluded renamed_res in
-  (loc,new_ids,new_patl,new_res)
+  (loc,(new_ids,new_patl,new_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 = function
+  let rec is_free_in (loc, gt) = match gt with
     | GRef _ ->  false
-    | GVar(_,id') -> Id.compare id' id == 0
+    | GVar id' -> Id.compare id' id == 0
     | GEvar _ -> false
     | GPatVar _ -> false
-    | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
-    | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) ->
+    | GApp(rt,rtl) -> List.exists is_free_in (rt::rtl)
+    | GLambda(n,_,t,b) | GProd(n,_,t,b) ->
 	let check_in_b =
 	  match n with
 	    | Name id' -> not (Id.equal id' id)
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
-    | GLetIn(_,n,b,t,c) ->
+    | GLetIn(n,b,t,c) ->
 	let check_in_c =
 	  match n with
 	    | Name id' -> not (Id.equal id' id)
 	    | _ -> true
 	in
 	is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c)
-    | GCases(_,_,_,el,brl) ->
+    | GCases(_,_,el,brl) ->
 	(List.exists (fun (e,_) -> is_free_in e) el) ||
 	  List.exists is_free_in_br brl
-    | GLetTuple(_,nal,_,b,t) ->
+    | GLetTuple(nal,_,b,t) ->
 	let check_in_nal =
 	  not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal)
 	in
 	is_free_in t  || (check_in_nal && is_free_in b)
 
-    | GIf(_,cond,_,br1,br2) ->
+    | GIf(cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
     | GRec _ -> raise (UserError(None,str "Not handled GRec"))
     | GSort _ -> false
     | 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
-  and is_free_in_br (_,ids,_,rt) =
+    | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
+    | GCast (b,CastCoerce) -> is_free_in b
+  and is_free_in_br (_,(ids,_,rt)) =
     (not (Id.List.mem id ids)) && is_free_in rt
   in
   is_free_in
@@ -452,60 +445,55 @@ let rec pattern_to_term pt = Loc.with_unloc (function
 
 
 let replace_var_by_term x_id term =
-  let rec replace_var_by_pattern rt =
+  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 -> term
+      | GVar id when Id.compare id x_id == 0 -> Loc.obj term
       | GVar _ -> rt
       | GEvar _ -> rt
       | GPatVar _ -> rt
-      | GApp(loc,rt',rtl) ->
-	  GApp(loc,
-	       replace_var_by_pattern 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(loc,name,k,t,b) ->
-	  GLambda(loc,
-		  name,
+      | GLambda(Name id,_,_,_) 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(loc,name,k,t,b) ->
-	  GProd(loc,
-		  name,
+      | GProd(Name id,_,_,_) 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(loc,name,def,typ,b) ->
-	  GLetIn(loc,
-		 name,
+      | GLetIn(Name id,_,_,_) 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,_,_,_)
 	  when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal  ->
 	  rt
-      | GLetTuple(loc,nal,(na,rto),def,b) ->
-	  GLetTuple(loc,
-		    nal,
+      | GLetTuple(nal,(na,rto),def,b) ->
+	  GLetTuple(nal,
 		    (na,Option.map replace_var_by_pattern rto),
 		    replace_var_by_pattern def,
 		    replace_var_by_pattern b
 		   )
-      | GCases(loc,sty,infos,el,brl) ->
-	  GCases(loc,sty,
+      | GCases(sty,infos,el,brl) ->
+	  GCases(sty,
 		 infos,
 		 List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
 		 List.map replace_var_by_pattern_br brl
 		)
-      | GIf(loc,b,(na,e_option),lhs,rhs) ->
-	  GIf(loc, replace_var_by_pattern b,
+      | GIf(b,(na,e_option),lhs,rhs) ->
+	  GIf(replace_var_by_pattern b,
 	      (na,Option.map replace_var_by_pattern e_option),
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
@@ -513,13 +501,13 @@ let replace_var_by_term x_id term =
       | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
-      | GCast(loc,b,c) ->
-	  GCast(loc,replace_var_by_pattern b,
+      | GCast(b,c) ->
+	  GCast(replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
-  and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
+  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
-    else (loc,idl,patl,replace_var_by_pattern res)
+    else (loc,(idl,patl,replace_var_by_pattern res))
   in
   replace_var_by_pattern
 
@@ -590,22 +578,22 @@ let id_of_name = function
 
 (* TODO: finish Rec caes *)
 let ids_of_glob_constr c =
-  let rec ids_of_glob_constr acc c =
+  let rec ids_of_glob_constr acc (loc, c) =
     let idof = id_of_name in
     match c with
-      | GVar (_,id) -> id::acc
-      | GApp (loc,g,args) ->
+      | GVar id -> id::acc
+      | GApp (g,args) ->
           ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
-      | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
-      | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
-      | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
-      | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
-      | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
-      | GLetTuple (_,nal,(na,po),b,c) ->
+      | GLambda (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+      | GProd (na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
+      | GLetIn (na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc
+      | GCast (c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
+      | GCast (c,CastCoerce) -> ids_of_glob_constr [] c @ acc
+      | GIf (c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
+      | GLetTuple (nal,(na,po),b,c) ->
           List.map idof nal @ ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
-      | GCases (loc,sty,rtntypopt,tml,brchl) ->
-	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
+      | GCases (sty,rtntypopt,tml,brchl) ->
+	  List.flatten (List.map (fun (_,(idl,patl,c)) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
@@ -617,49 +605,46 @@ let ids_of_glob_constr c =
 
 
 let zeta_normalize =
-  let rec zeta_normalize_term rt =
+  let rec zeta_normalize_term (loc, rt) = Loc.tag ~loc @@
     match rt with
       | GRef _ -> rt
       | GVar _ -> rt
       | GEvar _ -> rt
       | GPatVar _ -> rt
-      | GApp(loc,rt',rtl) ->
-	  GApp(loc,
-	       zeta_normalize_term rt',
+      | GApp(rt',rtl) ->
+	  GApp(zeta_normalize_term rt',
 	       List.map zeta_normalize_term rtl
 	      )
-      | GLambda(loc,name,k,t,b) ->
-	  GLambda(loc,
-		  name,
+      | GLambda(name,k,t,b) ->
+	  GLambda(name,
 		  k,
 		  zeta_normalize_term t,
 		  zeta_normalize_term b
 		 )
-      | GProd(loc,name,k,t,b) ->
-	  GProd(loc,
-		name,
+      | GProd(name,k,t,b) ->
+	  GProd(name,
 	        k,
 		zeta_normalize_term t,
 		zeta_normalize_term b
 		 )
-      | GLetIn(_,Name id,def,typ,b) ->
-	  zeta_normalize_term (replace_var_by_term id def b)
-      | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b
-      | GLetTuple(loc,nal,(na,rto),def,b) ->
-	  GLetTuple(loc,
-		    nal,
+      | GLetIn(Name id,def,typ,b) ->
+	  Loc.obj @@ zeta_normalize_term (replace_var_by_term id def b)
+      | GLetIn(Anonymous,def,typ,b) ->
+          Loc.obj @@ zeta_normalize_term b
+      | GLetTuple(nal,(na,rto),def,b) ->
+	  GLetTuple(nal,
 		    (na,Option.map zeta_normalize_term rto),
 		    zeta_normalize_term def,
 		    zeta_normalize_term b
 		   )
-      | GCases(loc,sty,infos,el,brl) ->
-	  GCases(loc,sty,
+      | GCases(sty,infos,el,brl) ->
+	  GCases(sty,
 		 infos,
 		 List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
 		 List.map zeta_normalize_br brl
 		)
-      | GIf(loc,b,(na,e_option),lhs,rhs) ->
-	  GIf(loc, zeta_normalize_term b,
+      | GIf(b,(na,e_option),lhs,rhs) ->
+	  GIf(zeta_normalize_term b,
 	      (na,Option.map zeta_normalize_term e_option),
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
@@ -667,11 +652,11 @@ let zeta_normalize =
       | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
-      | GCast(loc,b,c) ->
-	  GCast(loc,zeta_normalize_term b,
+      | GCast(b,c) ->
+	  GCast(zeta_normalize_term b,
                 Miscops.map_cast_type zeta_normalize_term c)
-  and zeta_normalize_br (loc,idl,patl,res) =
-    (loc,idl,patl,zeta_normalize_term res)
+  and zeta_normalize_br (loc,(idl,patl,res)) =
+    (loc,(idl,patl,zeta_normalize_term res))
   in
   zeta_normalize_term
 
@@ -687,33 +672,34 @@ let expand_as =
 	  Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl)
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
-  let rec expand_as map rt =
+  let rec expand_as map (loc, rt) =
+    Loc.tag ~loc @@
     match rt with
       | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt
-      | GVar(_,id) ->
+      | GVar id ->
 	  begin
 	    try
-	      Id.Map.find id map
+	      Loc.obj @@ Id.Map.find id map
 	    with Not_found -> rt
 	  end
-      | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
-      | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b)
-      | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b)
-      | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b)
-      | GLetTuple(loc,nal,(na,po),v,b) ->
-	  GLetTuple(loc,nal,(na,Option.map (expand_as map) po),
+      | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
+      | GLambda(na,k,t,b) -> GLambda(na,k,expand_as map t, expand_as map b)
+      | GProd(na,k,t,b) -> GProd(na,k,expand_as map t, expand_as map b)
+      | GLetIn(na,v,typ,b) -> GLetIn(na, expand_as map v,Option.map (expand_as map) typ,expand_as map b)
+      | GLetTuple(nal,(na,po),v,b) ->
+	  GLetTuple(nal,(na,Option.map (expand_as map) po),
 		    expand_as map v, expand_as map b)
-      | GIf(loc,e,(na,po),br1,br2) ->
-	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
+      | GIf(e,(na,po),br1,br2) ->
+	  GIf(expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
-      | GCast(loc,b,c) ->
-	  GCast(loc,expand_as map b,
+      | GCast(b,c) ->
+	  GCast(expand_as map b,
 		Miscops.map_cast_type (expand_as map) c)
-      | GCases(loc,sty,po,el,brl) ->
-	  GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+      | 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)
+  and expand_as_br map (loc,(idl,cpl,rt)) =
+    (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
   in
   expand_as Id.Map.empty