[location] Switch glob_constr to Loc.located

7 files changed, 259 insertions, 278 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 85d465a4bb..07a0d5a505 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -274,10 +274,10 @@ let make_discr_match_el  =
 *)
 let make_discr_match_brl i =
   List.map_i
-    (fun j (_,idl,patl,_) ->
+    (fun j (_,(idl,patl,_)) -> Loc.tag @@
        if Int.equal j i
-       then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
-       else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
+       then (idl,patl, mkGRef (Lazy.force coq_True_ref))
+       else (idl,patl, mkGRef (Lazy.force coq_False_ref))
     )
     0
 (*
@@ -464,13 +464,13 @@ 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 =
+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 _  ->
+    | _, 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,20 +482,20 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	    (mk_result [] [] avoid)
 	in
 	begin
-	  match f with
+	  match Loc.obj f with
 	    | GLambda _  -> 
 		let rec aux t l = 
 		  match l with 
 		    | [] -> t
-		    | u::l -> 
+		    | u::l -> Loc.tag @@
 			match t with 
-			  | GLambda(loc,na,_,nat,b) -> 
-			      GLetIn(Loc.ghost,na,u,None,aux b l)
+			  | loc, GLambda(na,_,nat,b) -> 
+			      GLetIn(na,u,None,aux b l)
 			  | _ -> 
-			      GApp(Loc.ghost,t,l)
+			      GApp(t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
-	    | GVar(_,id) when Id.Set.mem id funnames ->
+	    | GVar id when Id.Set.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
 		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
@@ -536,7 +536,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		      args_res.result
 		}
 	    | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *)
-	    | GLetIn(_,n,v,t,b) ->
+	    | GLetIn(n,v,t,b) ->
 		(* if we have [(let x := v in b) t1 ... tn] ,
 		   we discard our work and compute the list of constructor for
 		   [let x = v in (b t1 ... tn)] up to alpha conversion
@@ -550,7 +550,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (GVar(Loc.ghost,id))
+			    (Loc.tag @@ GVar id)
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -568,7 +568,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
-	    | GCast(_,b,_) ->
+	    | GCast(b,_) ->
 		(* for an applied cast we just trash the cast part
 		   and restart the work.
 
@@ -579,7 +579,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 +594,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 +604,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
-    | GLetIn(loc,n,v,typ,b) ->
+    | loc, 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 -> GCast (loc,v,CastConv t) in
+        let v = match typ with None -> v | Some t -> Loc.tag ~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 +622,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,_) =
@@ -642,7 +642,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	assert (Int.equal (Array.length case_pats) 2);
 	let brl =
 	  List.map_i
-	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
+	    (fun i x -> Loc.tag ([],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
 	in
@@ -651,7 +651,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
@@ -673,14 +673,14 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
 	  assert (Int.equal (Array.length case_pats) 1);
 	  let br =
-	    (Loc.ghost,[],[case_pats.(0)],e)
+	    (Loc.ghost,([],[case_pats.(0)],e))
 	  in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  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)
@@ -740,7 +740,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
 	(* alpha conversion to prevent name clashes *)
-	let _,idl,patl,return = alpha_br avoid br in
+	let _,(idl,patl,return) = alpha_br avoid br in
 	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
@@ -862,9 +862,9 @@ let is_res id =
 
 
 
-let same_raw_term rt1 rt2 = 
+let same_raw_term (_,rt1) (_,rt2) = 
   match rt1,rt2 with 
-    | GRef(_,r1,_), GRef (_,r2,_) -> Globnames.eq_gr r1 r2
+    | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
@@ -897,15 +897,15 @@ 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) ->
+    | _, 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 ->
+	    | _, GApp(((_, GVar(res_id)) as res_rt),args') when is_res res_id ->
 		begin
 		  match args' with
-		    | (GVar(_,this_relname))::args' ->
+		    | (_, (GVar this_relname))::args' ->
 			(*i The next call to mk_rel_id is
 			  valid since we are constructing the graph
 			  Ensures by: obvious
@@ -927,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
-	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;GVar(loc3,id);rt])
+	    | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;(loc3, GVar id);rt])
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
 		begin
@@ -964,9 +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 =
-		       GApp(Loc.ghost,
-			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
+		    let rt_typ = Loc.tag @@
+		       GApp(Loc.tag @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
 				 env (Evd.from_env env)
@@ -976,7 +975,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt])
+		      Loc.tag ~loc:loc1 @@ GApp(Loc.tag ~loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ~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
@@ -1045,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
 		  *)
-	    | GApp(loc1,GRef(loc2,eq_as_ref,_),[ty;rt1;rt2])
+	    | loc1, GApp((loc2, GRef(eq_as_ref,_)),[ty;rt1;rt2])
 		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
@@ -1096,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
@@ -1115,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
-		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+		  Loc.tag @@ 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
-    | GLetIn(loc,n,v,t,b) ->
+    | loc, GLetIn(n,v,t,b) ->
 	begin
-          let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in
+          let t = match t with None -> v | Some t -> Loc.tag ~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
@@ -1138,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)
-	    | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *)
+	    | _ -> Loc.tag @@ 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
@@ -1164,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) *)
 (* 	    | _ -> *)
-	  GLetTuple(Loc.ghost,nal,(na,None),t,new_b),
+	  Loc.tag @@ GLetTuple(nal,(na,None),t,new_b),
 		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
@@ -1190,16 +1189,16 @@ 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 = function
+let rec compute_cst_params relnames params gt = Loc.with_unloc (function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames ->
+  | GApp((_, GVar relname'),rtl) when Id.Set.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
-  | GApp(_,f,args) ->
+  | GApp(f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
-  | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) ->
+  | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
-  | GLetIn(_,_,v,t,b) ->
+  | GLetIn(_,v,t,b) ->
       let v_params = compute_cst_params relnames params v in
       let t_params = Option.fold_left (compute_cst_params relnames) v_params t in
       compute_cst_params relnames t_params b
@@ -1210,10 +1209,11 @@ let rec compute_cst_params relnames params = function
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
+  ) gt
 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',(_, 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 51ca8c4717..01e607412a 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
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 84359a36b7..25d79582f3 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -82,11 +82,8 @@ val alpha_rt : Id.t list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
 val alpha_br : Id.t list ->
-    Loc.t * Id.t list * Glob_term.cases_pattern list *
-    Glob_term.glob_constr ->
-    Loc.t * Id.t list * Glob_term.cases_pattern list *
-    Glob_term.glob_constr
-
+  Glob_term.cases_clause ->
+  Glob_term.cases_clause
 
 (* Reduction function *)
 val replace_var_by_term  :
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6ee7553231..cad96946ca 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -190,18 +190,18 @@ 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 = function
-    | GVar(_,id) -> check_id id names
+  let rec lookup names (loc, gt) = match gt with
+    | GVar(id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
-    | GCast(_,b,_) -> lookup names b
+    | GCast(b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
-    | GIf(_,b,_,lhs,rhs) ->
+    | GIf(b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
-    | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) ->
+    | GProd(na,_,t,b) | GLambda(na,_,t,b) ->
 	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
-    | GLetIn(_,na,b,t,c) ->
+    | GLetIn(na,b,t,c) ->
 	lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
-    | GLetTuple(_,nal,_,t,b) -> lookup names t ||
+    | GLetTuple(nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
 	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
@@ -209,11 +209,11 @@ let is_rec names =
 	     nal
 	  )
 	  b
-    | GApp(_,f,args) -> List.exists (lookup names) (f::args)
-    | GCases(_,_,_,el,brl) ->
+    | GApp(f,args) -> List.exists (lookup names) (f::args)
+    | GCases(_,_,el,brl) ->
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
-  and lookup_br names (_,idl,_,rt) =
+  and lookup_br names (_,(idl,_,rt)) =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7b0d7d27d7..8f0c986242 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -69,9 +69,9 @@ let chop_rlambda_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt 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
+	match Loc.obj rt 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
 	  | _ ->
 	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
@@ -83,8 +83,8 @@ let chop_rprod_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt with
-	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+	match Loc.obj rt 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
   chop_prod_n []
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 29de56478b..9dc1d48df3 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
+      | _, 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 c1 c2 id1 id2 shift filter_shift_stable =
+let rec merge_app (loc1, c1) (loc2, c2) id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match c1 , c2 with
-    | GApp(_,f1, arr1), GApp(_,f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
+  match c1, c2 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
-        GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args)
-    | GApp(_,f1, arr1), GApp(_,f2,arr2)  -> raise NoMerge
-    | GLetIn(_,nme,bdy,typ,trm) , _ ->
+        Loc.tag @@ GApp ((Loc.tag @@ 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 c2 id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
-    | _, GLetIn(_,nme,bdy,typ,trm) ->
+        let newtrm = merge_app trm (loc2, c2) id1 id2 shift filter_shift_stable in
+        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+    | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3!\n" in
-        let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+        let newtrm = merge_app (loc1, c1) trm id1 id2 shift filter_shift_stable in
+        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
-let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
+let rec merge_app_unsafe (l1, c1) (l2, c2) shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
   match c1 , c2 with
-    | GApp(_,f1, arr1), GApp(_,f2,arr2) ->
+    | GApp(f1, arr1), GApp(f2,arr2) ->
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args)
+        Loc.tag @@ GApp (Loc.tag @@ GVar shift.ident, args)
           (* FIXME: what if the function appears in the body of the let? *)
-    | GLetIn(_,nme,bdy,typ,trm) , _ ->
+    | GLetIn(nme,bdy,typ,trm) , _ ->
       let _ = prstr "\nICI2 '!\n" in
-        let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
-    | _, GLetIn(_,nme,bdy,typ,trm) ->
+        let newtrm = merge_app_unsafe trm (l2, c2) shift filter_shift_stable in
+        Loc.tag @@ GLetIn(nme,bdy,typ,newtrm)
+    | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3 '!\n" in
-        let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        GLetIn(Loc.ghost,nme,bdy,typ,newtrm)
+        let newtrm = merge_app_unsafe (l1, c1) trm shift filter_shift_stable in
+        Loc.tag @@ 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 (_, 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 (_, 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 (_, GApp(f,_)) when isVarf nme f -> raise (Found 0)
               | _ -> ())
           ltyp);
     false
@@ -633,7 +633,7 @@ 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 ->
+            | _, 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
-        GProd (Loc.ghost,nme,Explicit,traw,t2)
+        Loc.tag @@ GProd (nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ee7b33227c..c796fe7a2d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -172,7 +172,6 @@ let simpl_iter clause =
 let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
   let open Term in
   fun al fterm ->
-    let d0 = Loc.ghost in
     let rev_x_id_l =
       (
 	List.fold_left
@@ -189,16 +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 =
-      GCases
-	(d0,RegularStyle,None,
-	 [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
+      Loc.tag @@
+       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),
 	  (Anonymous,None)],
-	 [d0, [v_id], [d0,PatCstr((destIndRef
-				     (delayed_force coq_sig_ref),1),
-			       [d0, PatVar(Name v_id);
-				d0, PatVar(Anonymous)],
-			       Anonymous)],
-	  GVar(d0,v_id)])
+	 [Loc.tag ([v_id], [Loc.tag @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+			   [Loc.tag @@ PatVar(Name v_id); Loc.tag @@ PatVar Anonymous],
+                           Anonymous)],
+	    Loc.tag @@ GVar v_id)])
     in
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context