[location] Switch glob_constr to Loc.located

6 files changed, 292 insertions, 297 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5314859358..347c49f448 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -348,8 +348,8 @@ let find_tomatch_tycon evdref env loc = function
       empty_tycon,None
 
 let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
-  let loc = Some (loc_of_glob_constr tomatch) in
-  let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
+  let loc = loc_of_glob_constr tomatch in
+  let tycon,realnames = find_tomatch_tycon evdref env (Some loc) indopt in
   let j = typing_fun tycon env evdref tomatch in
   let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in
   evdref := evd;
@@ -357,7 +357,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
   let t =
     try try_find_ind env !evdref typ realnames
     with Not_found ->
-      unify_tomatch_with_patterns evdref env loc typ pats realnames in
+      unify_tomatch_with_patterns evdref env (Some loc) typ pats realnames in
   (j.uj_val,t)
 
 let coerce_to_indtype typing_fun evdref env matx tomatchl = 
@@ -1535,7 +1535,7 @@ substituer après par les initiaux *)
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in astterm *)
 let matx_of_eqns env eqns =
-  let build_eqn (loc,ids,lpat,rhs) =
+  let build_eqn (loc,(ids,lpat,rhs)) =
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
     let rhs =
@@ -2059,8 +2059,8 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole =
-  GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole = Loc.tag @@
+  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
@@ -2160,13 +2160,13 @@ let vars_of_ctx sigma ctx =
       match decl with
 	| LocalDef (na,t',t) when is_topvar sigma t' ->
 	    prev,
-	    (GApp (Loc.ghost,
-		(GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), 
-		   [hole; GVar (Loc.ghost, prev)])) :: vars
+	    (Loc.tag @@ GApp (
+		(Loc.tag @@ GRef (delayed_force coq_eq_refl_ref, None)), 
+		   [hole; Loc.tag @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
-	      | Name n -> n, GVar (Loc.ghost, n) :: vars)
+	      | Name n -> n, (Loc.tag @@ GVar n) :: vars)
       ctx (Id.of_string "vars_of_ctx_error", [])
   in List.rev y
 
@@ -2289,13 +2289,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
-	   let bref = GVar (Loc.ghost, branch_name) in
+	   let bref = Loc.tag @@ GVar branch_name in
 	     match vars_of_ctx !evdref rhs_rels with
 		 [] -> bref
-	       | l -> GApp (Loc.ghost, bref, l)
+	       | l  -> Loc.tag @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> GApp (Loc.ghost, branch, [ hole ])
+	     Some _ -> Loc.tag @@ GApp (branch, [ hole ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f3018ac64b..05d6a1ad4a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -331,20 +331,20 @@ let is_nondep_branch sigma c l =
 
 let extract_nondep_branches test c b l =
   let rec strip l r =
-    match r,l with
-      | r, [] -> r
-      | GLambda (_,_,_,_,t), false::l -> strip l t
-      | GLetIn (_,_,_,_,t), true::l -> strip l t
+    match snd r,l with
+      | r', [] -> r
+      | GLambda (_,_,_,t), false::l -> strip l t
+      | GLetIn (_,_,_,t), true::l -> strip l t
       (* FIXME: do we need adjustment? *)
       | _,_ -> assert false in
   if test c l then Some (strip l b) else None
 
 let it_destRLambda_or_LetIn_names l c =
   let rec aux l nal c =
-    match c, l with
+    match snd c, l with
       | _, [] -> (List.rev nal,c)
-      | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c
-      | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c
+      | GLambda (na,_,_,c), false::l -> aux l (na::nal) c
+      | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c
       | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
       | _, false::l ->
           (* eta-expansion *)
@@ -355,11 +355,11 @@ let it_destRLambda_or_LetIn_names l c =
 	    x
 	  in
 	  let x = next (free_glob_vars c) in
-	  let a = GVar (dl,x) in
+	  let a = Loc.tag @@ GVar x in
 	  aux l (Name x :: nal)
             (match c with
-              | GApp (loc,p,l) -> GApp (loc,p,l@[a])
-              | _ -> (GApp (dl,c,[a])))
+              | loc, GApp (p,l) -> (loc, GApp (p,l@[a]))
+              | _ -> Loc.tag @@ GApp (c,[a]))
   in aux l [] c
 
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
@@ -375,12 +375,12 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
         | None -> Anonymous, None, None
         | Some p ->
             let nl,typ = it_destRLambda_or_LetIn_names k p in
-	    let n,typ = match typ with
-              | GLambda (_,x,_,t,c) -> x, c
+	    let n,typ = match snd typ with
+              | GLambda (x,_,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all (Name.equal Anonymous) nl then None
-	      else Some (dl,(indsp,nl)) in
+	      else Some (Loc.tag (indsp,nl)) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -397,25 +397,25 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       else
 	st
     with Not_found -> st
-  in
+  in Loc.tag @@
   match tag, aliastyp with
   | LetStyle, None ->
       let bl' = Array.map detype bl in
       let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in
-      GLetTuple (dl,nal,(alias,pred),tomatch,d)
+      GLetTuple (nal,(alias,pred),tomatch,d)
   | IfStyle, None ->
       let bl' = Array.map detype bl in
       let nondepbrs =
 	Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in
       if Array.for_all ((!=) None) nondepbrs then
-	GIf (dl,tomatch,(alias,pred),
+	GIf (tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
 	let eqnl = detype_eqns constructs constagsl bl in
-	GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+	GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
       let eqnl = detype_eqns constructs constagsl bl in
-      GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+      GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort sigma = function
   | Prop Null -> GProp
@@ -423,7 +423,7 @@ let detype_sort sigma = function
   | Type u ->
     GType
       (if !print_universes
-       then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
+       then [Loc.tag @@ Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -431,36 +431,36 @@ type binder_kind = BProd | BLambda | BLetIn
 (**********************************************************************)
 (* Main detyping function                                             *)
 
-let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
+let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
 let set_detype_anonymous f = detype_anonymous := f
 
 let detype_level sigma l =
-  GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
+  GType (Some (Loc.tag @@ Pp.string_of_ppcmds (Termops.pr_evd_level sigma l)))
 
 let detype_instance sigma l = 
   let l = EInstance.kind sigma l in
   if Univ.Instance.is_empty l then None
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
-let rec detype flags avoid env sigma t =
+let rec detype flags avoid env sigma t = Loc.tag @@
   match EConstr.kind sigma (collapse_appl sigma t) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
-	 | Name id   -> GVar (dl, id)
-	 | Anonymous -> !detype_anonymous dl n
+	 | Name id   -> GVar id
+	 | Anonymous -> snd @@ !detype_anonymous n
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in GVar (dl, Id.of_string s))
+	 in GVar (Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         (* using numbers to be unparsable *)
-	GEvar (dl, Id.of_string ("M" ^ string_of_int n), [])
+	GEvar (Id.of_string ("M" ^ string_of_int n), [])
     | Var id ->
-	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
-	 with Not_found -> GVar (dl, id))
-    | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s))
+	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
+	 with Not_found -> GVar id)
+    | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
-        detype flags avoid env sigma c1
+        snd (detype flags avoid env sigma c1)
     | Cast (c1,k,c2) ->
         let d1 = detype flags avoid env sigma c1 in
 	let d2 = detype flags avoid env sigma c2 in
@@ -469,34 +469,34 @@ let rec detype flags avoid env sigma t =
     | NATIVEcast -> CastNative d2
     | _ -> CastConv d2
     in
-	GCast(dl,d1,cast)
-    | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c
-    | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c
-    | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c
+	GCast(d1,cast)
+    | Prod (na,ty,c) -> snd @@ detype_binder flags BProd avoid env sigma na None ty c
+    | Lambda (na,ty,c) -> snd @@ detype_binder flags BLambda avoid env sigma na None ty c
+    | LetIn (na,b,ty,c) -> snd @@ detype_binder flags BLetIn avoid env sigma na (Some b) ty c
     | App (f,args) ->
       let mkapp f' args' = 
- 	match f' with
- 	| GApp (dl',f',args'') -> 
- 	  GApp (dl,f',args''@args')
- 	| _ -> GApp (dl,f',args')
+ 	match snd f' with
+ 	| GApp (f',args'') -> 
+ 	  GApp (f',args''@args')
+ 	| _ -> GApp (f',args')
       in
 	mkapp (detype flags avoid env sigma f)
 	  (Array.map_to_list (detype flags avoid env sigma) args)
-    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u)
+    | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
 	let pb = Environ.lookup_projection p (snd env) in
 	let pars = pb.Declarations.proj_npars in
-	let hole = GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
+	let hole = Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
 	let args = List.make pars hole in
- 	  GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
+ 	  GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None),
 		(args @ [detype flags avoid env sigma c]))
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
 	with _ ->
 	    (* lax mode, used by debug printers only *) 
-	  GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), 
+	  GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p), None), 
 		[detype flags avoid env sigma c])
       else 
 	if print_primproj_compatibility () && Projection.unfolded p then
@@ -514,12 +514,12 @@ let rec detype flags avoid env sigma t =
 		substl (c :: List.rev args) body'
 	    with Retyping.RetypeError _ | Not_found -> 
 	      anomaly (str"Cannot detype an unfolded primitive projection.")
-	  in detype flags avoid env sigma c'
+	  in snd @@ detype flags avoid env sigma c'
 	else
 	  if print_primproj_params () then
 	    try
 	      let c = Retyping.expand_projection (snd env) sigma p c [] in
-		detype flags avoid env sigma c
+		snd @@ detype flags avoid env sigma c
 	    with Retyping.RetypeError _ -> noparams ()
 	  else noparams ()
 
@@ -546,14 +546,15 @@ let rec detype flags avoid env sigma t =
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
           (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
-        GEvar (dl,id,
+        GEvar (id,
                List.map (on_snd (detype flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
-	GRef (dl, IndRef ind_sp, detype_instance sigma u)
+	GRef (IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
-	GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
+	GRef (ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
 	let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
+	snd @@
 	detype_case comp (detype flags avoid env sigma)
 	  (detype_eqns flags avoid env sigma ci comp)
 	  (is_nondep_branch sigma) avoid
@@ -574,7 +575,7 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let v = Array.map3
     (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
-  GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -590,7 +591,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
   let v = Array.map2
     (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t))
     bodies tys in
-  GRec(dl,GCoFix n,Array.of_list (List.rev lfi),
+  GRec(GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -635,7 +636,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
+    List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
     Array.to_list
@@ -644,7 +645,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
 and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
   let make_pat x avoid env b body ty ids =
     if force_wildcard () && noccurn sigma 1 b then
-      Loc.tag @@ PatVar (Anonymous),avoid,(add_name Anonymous body ty env),ids
+      Loc.tag @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids
     else
       let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
       let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
@@ -652,9 +653,9 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
   in
   let rec buildrec ids patlist avoid env l b =
     match EConstr.kind sigma b, l with
-      | _, [] ->
-        (dl, Id.Set.elements ids,
-         [Loc.tag ~loc:dl @@ PatCstr(constr, List.rev patlist,Anonymous)],
+      | _, [] -> Loc.tag @@
+        (Id.Set.elements ids,
+         [Loc.tag @@ PatCstr(constr, List.rev patlist,Anonymous)],
          detype flags avoid env sigma b)
       | Lambda (x,t,b), false::l ->
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
@@ -668,7 +669,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
 	    buildrec ids patlist avoid env l c
 
       | _, true::l ->
-	    let pat = Loc.tag ~loc:dl @@ PatVar Anonymous in
+	    let pat = Loc.tag @@ PatVar Anonymous in
             buildrec ids (pat::patlist) avoid env l b
 
       | _, false::l ->
@@ -683,21 +684,21 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
   in
   buildrec Id.Set.empty [] avoid env construct_nargs branch
 
-and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
+and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = Loc.tag @@
   let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
   let na',avoid' = match bk with
   | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
   | _ -> compute_displayed_name_in sigma flag avoid na c in
   let r =  detype flags avoid' (add_name na' body ty env) sigma c in
   match bk with
-  | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
-  | BLambda -> GLambda (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r)
+  | BProd   -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r)
+  | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r)
   | BLetIn ->
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
       let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
-      GLetIn (dl, na', c, t, r)
+      GLetIn (na', c, t, r)
 
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
@@ -741,11 +742,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
     | Name id -> Name (convert_id cl id)
     | Anonymous -> Anonymous
   in
-  let rec detype_closed_glob cl = function
-    | GVar (loc,id) ->
+  let rec detype_closed_glob cl cg = Loc.map (function
+    | GVar id ->
         (* if [id] is bound to a name. *)
         begin try
-          GVar(loc,Id.Map.find id cl.idents)
+          GVar(Id.Map.find id cl.idents)
         (* if [id] is bound to a typed term *)
         with Not_found -> try
           (* assumes [detype] does not raise [Not_found] exceptions *)
@@ -755,38 +756,39 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
              [Printer.pr_constr_under_binders_env] does. *)
           let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
           let env = push_rel_context assums env in
-          detype ?lax isgoal avoid env sigma c
+          snd @@ detype ?lax isgoal avoid env sigma c
         (* if [id] is bound to a [closed_glob_constr]. *)
         with Not_found -> try
           let {closure;term} = Id.Map.find id cl.untyped in
-          detype_closed_glob closure term
+          snd @@ detype_closed_glob closure term
         (* Otherwise [id] stands for itself *)
         with Not_found ->
-         GVar(loc,id)
+         GVar id
         end
-    | GLambda (loc,id,k,t,c) ->
+    | GLambda (id,k,t,c) ->
         let id = convert_name cl id in
-        GLambda(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GProd (loc,id,k,t,c) ->
+        GLambda(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GProd (id,k,t,c) ->
         let id = convert_name cl id in
-        GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GLetIn (loc,id,b,t,e) ->
+        GProd(id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GLetIn (id,b,t,e) ->
         let id = convert_name cl id in
-        GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
-    | GLetTuple (loc,ids,(n,r),b,e) ->
+        GLetIn(id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
+    | GLetTuple (ids,(n,r),b,e) ->
         let ids = List.map (convert_name cl) ids in
         let n = convert_name cl n in
-        GLetTuple (loc,ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e)
-    | GCases (loc,sty,po,tml,eqns) ->
+        GLetTuple (ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e)
+    | GCases (sty,po,tml,eqns) ->
         let (tml,eqns) =
           Glob_ops.map_pattern_binders (fun na -> convert_name cl na) tml eqns
         in
         let (tml,eqns) =
           Glob_ops.map_pattern (fun c -> detype_closed_glob cl c) tml eqns
         in
-        GCases(loc,sty,po,tml,eqns)
+        GCases(sty,po,tml,eqns)
     | c ->
-        Glob_ops.map_glob_constr (detype_closed_glob cl) c
+        snd @@ Glob_ops.map_glob_constr (detype_closed_glob cl) cg
+    ) cg
   in
   detype_closed_glob t.closure t.term
 
@@ -804,41 +806,41 @@ let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
-let rec subst_glob_constr subst raw =
+let rec subst_glob_constr subst (loc, raw) = Loc.tag ~loc @@
   match raw with
-  | GRef (loc,ref,u) ->
+  | GRef (ref,u) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
+         snd @@ detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)
 
   | GVar _ -> raw
   | GEvar _ -> raw
   | GPatVar _ -> raw
 
-  | GApp (loc,r,rl) ->
+  | GApp (r,rl) ->
       let r' = subst_glob_constr subst r
       and rl' = List.smartmap (subst_glob_constr subst) rl in
 	if r' == r && rl' == rl then raw else
-	  GApp(loc,r',rl')
+	  GApp(r',rl')
 
-  | GLambda (loc,n,bk,r1,r2) ->
+  | GLambda (n,bk,r1,r2) ->
       let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  GLambda (loc,n,bk,r1',r2')
+	  GLambda (n,bk,r1',r2')
 
-  | GProd (loc,n,bk,r1,r2) ->
+  | GProd (n,bk,r1,r2) ->
       let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  GProd (loc,n,bk,r1',r2')
+	  GProd (n,bk,r1',r2')
 
-  | GLetIn (loc,n,r1,t,r2) ->
+  | GLetIn (n,r1,t,r2) ->
       let r1' = subst_glob_constr subst r1 in
-      let t' = Option.smartmap (subst_glob_constr subst) t in
       let r2' = subst_glob_constr subst r2 in
+      let t' = Option.smartmap (subst_glob_constr subst) t in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
-	  GLetIn (loc,n,r1',t',r2')
+	  GLetIn (n,r1',t',r2')
 
-  | GCases (loc,sty,rtno,rl,branches) ->
+  | GCases (sty,rtno,rl,branches) ->
       let rtno' = Option.smartmap (subst_glob_constr subst) rtno
       and rl' = List.smartmap (fun (a,x as y) ->
         let a' = subst_glob_constr subst a in
@@ -849,33 +851,33 @@ let rec subst_glob_constr subst raw =
             if sp == sp' then t else (loc,((sp',i),y))) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = List.smartmap
-			(fun (loc,idl,cpl,r as branch) ->
+			(fun (loc,(idl,cpl,r) as branch) ->
 			   let cpl' =
 			     List.smartmap (subst_cases_pattern subst) cpl
 			   and r' = subst_glob_constr subst r in
 			     if cpl' == cpl && r' == r then branch else
-			       (loc,idl,cpl',r'))
+			       (loc,(idl,cpl',r')))
 			branches
       in
 	if rtno' == rtno && rl' == rl && branches' == branches then raw else
-	  GCases (loc,sty,rtno',rl',branches')
+	  GCases (sty,rtno',rl',branches')
 
-  | GLetTuple (loc,nal,(na,po),b,c) ->
+  | GLetTuple (nal,(na,po),b,c) ->
       let po' = Option.smartmap (subst_glob_constr subst) po
       and b' = subst_glob_constr subst b
       and c' = subst_glob_constr subst c in
 	if po' == po && b' == b && c' == c then raw else
-          GLetTuple (loc,nal,(na,po'),b',c')
+          GLetTuple (nal,(na,po'),b',c')
 
-  | GIf (loc,c,(na,po),b1,b2) ->
+  | GIf (c,(na,po),b1,b2) ->
       let po' = Option.smartmap (subst_glob_constr subst) po
       and b1' = subst_glob_constr subst b1
       and b2' = subst_glob_constr subst b2
       and c' = subst_glob_constr subst c in
 	if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else
-          GIf (loc,c',(na,po'),b1',b2')
+          GIf (c',(na,po'),b1',b2')
 
-  | GRec (loc,fix,ida,bl,ra1,ra2) ->
+  | GRec (fix,ida,bl,ra1,ra2) ->
       let ra1' = Array.smartmap (subst_glob_constr subst) ra1
       and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in
       let bl' = Array.smartmap
@@ -885,11 +887,11 @@ let rec subst_glob_constr subst raw =
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
-	  GRec (loc,fix,ida,bl',ra1',ra2')
+	  GRec (fix,ida,bl',ra1',ra2')
 
   | GSort _ -> raw
 
-  | GHole (loc, knd, naming, solve) ->
+  | GHole (knd, naming, solve) ->
     let nknd = match knd with
     | Evar_kinds.ImplicitArg (ref, i, b) ->
       let nref, _ = subst_global subst ref in
@@ -898,12 +900,12 @@ let rec subst_glob_constr subst raw =
     in
     let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in
     if nsolve == solve && nknd == knd then raw
-    else GHole (loc, nknd, naming, nsolve)
+    else GHole (nknd, naming, nsolve)
 
-  | GCast (loc,r1,k) ->
+  | GCast (r1,k) ->
       let r1' = subst_glob_constr subst r1 in
       let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
-      if r1' == r1 && k' == k then raw else GCast (loc,r1',k')
+      if r1' == r1 && k' == k then raw else GCast (r1',k')
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
@@ -914,7 +916,7 @@ let simple_cases_matrix_of_branches ind brs =
       let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
       let map name = try Some (Nameops.out_name name) with Failure _ -> None in
       let ids = List.map_filter map nal in
-      (Loc.ghost,ids,[p],c))
+      Loc.tag @@ (ids,[p],c))
     brs
 
 let return_type_of_predicate ind nrealargs_tags pred =
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 4c6f9129f6..84da3652f1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -38,7 +38,7 @@ val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob
 val detype_case :
   bool -> (constr -> glob_constr) ->
   (constructor array -> bool list array -> constr array ->
-    (Loc.t * Id.t list * cases_pattern list * glob_constr) list) ->
+    (Id.t list * cases_pattern list * glob_constr) Loc.located list) ->
   (constr -> bool list -> bool) ->
   Id.t list -> inductive * case_style * bool list array * bool list ->
     constr option -> constr -> constr array -> glob_constr
@@ -54,7 +54,9 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> cl
 val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 
-val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
+(* XXX: This is a hack and should go away *)
+val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit
+
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 4cccaaf8ff..25ece5b8e9 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -22,10 +22,10 @@ let cases_predicate_names tml =
     | (tm,(na,None)) -> [na]
     | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml)
 
-let mkGApp loc p t =
-  match p with
-  | GApp (loc,f,l) -> GApp (loc,f,l@[t])
-  | _ -> GApp (loc,p,[t])
+let mkGApp loc p t = Loc.tag ~loc @@
+  match snd p with
+  | GApp (f,l) -> GApp (f,l@[t])
+  | _          -> GApp (p,[t])
 
 let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp1 = Option.map f obd in
@@ -59,46 +59,46 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
 | CastNative t1, CastNative t2 -> eq t1 t2
 | _ -> false
 
-let rec glob_constr_eq c1 c2 = match c1, c2 with
-| GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2
-| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
-| GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
+let rec glob_constr_eq (_loc1, c1) (_loc2, c2) = match c1, c2 with
+| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
+| GVar id1, GVar id2 -> Id.equal id1 id2
+| GEvar (id1, arg1), GEvar (id2, arg2) ->
   Id.equal id1 id2 &&
   List.equal instance_eq arg1 arg2
-| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
+| GPatVar (b1, pat1), GPatVar (b2, pat2) ->
   (b1 : bool) == b2 && Id.equal pat1 pat2
-| GApp (_, f1, arg1), GApp (_, f2, arg2) ->
+| GApp (f1, arg1), GApp (f2, arg2) ->
   glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2
-| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) ->
+| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) ->
   Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
   glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) ->
+| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) ->
   Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
   glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) ->
+| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) ->
   Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) ->
+| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) ->
   case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
   List.equal tomatch_tuple_eq tp1 tp2 &&
   List.equal cases_clause_eq cl1 cl2
-| GLetTuple (_, na1, (n1, p1), c1, t1), GLetTuple (_, na2, (n2, p2), c2, t2) ->
+| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) ->
   List.equal Name.equal na1 na2 && Name.equal n1 n2 &&
   Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
   glob_constr_eq t1 t2
-| GIf (_, m1, (pat1, p1), c1, t1), GIf (_, m2, (pat2, p2), c2, t2) ->
+| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
   glob_constr_eq m1 m2 && Name.equal pat1 pat2 &&
   Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 &&
   glob_constr_eq t1 t2
-| GRec (_, kn1, id1, decl1, c1, t1), GRec (_, kn2, id2, decl2, c2, t2) ->
+| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
   fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
   Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
   Array.equal glob_constr_eq c1 c2 &&
   Array.equal glob_constr_eq t1 t2
-| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2
-| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) ->
+| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
   Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
   Miscops.intro_pattern_naming_eq nam1 nam2
-| GCast (_, c1, t1), GCast (_, c2, t2) ->
+| GCast (c1, t1), GCast (c2, t2) ->
   glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2
 | _ -> false
 
@@ -109,7 +109,7 @@ and tomatch_tuple_eq (c1, p1) (c2, p2) =
   let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
   glob_constr_eq c1 c2 && eq_pred p1 p2
 
-and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) =
+and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) =
   List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 &&
   glob_constr_eq c1 c2
 
@@ -137,80 +137,82 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with
 and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && glob_constr_eq c1 c2
 
-let map_glob_constr_left_to_right f = function
-  | GApp (loc,g,args) ->
+let map_glob_constr_left_to_right f = Loc.map (function
+  | GApp (g,args) ->
       let comp1 = f g in
       let comp2 = Util.List.map_left f args in
-      GApp (loc,comp1,comp2)
-  | GLambda (loc,na,bk,ty,c) ->
+      GApp (comp1,comp2)
+  | GLambda (na,bk,ty,c) ->
       let comp1 = f ty in
       let comp2 = f c in
-      GLambda (loc,na,bk,comp1,comp2)
-  | GProd (loc,na,bk,ty,c) ->
+      GLambda (na,bk,comp1,comp2)
+  | GProd (na,bk,ty,c) ->
       let comp1 = f ty in
       let comp2 = f c in
-      GProd (loc,na,bk,comp1,comp2)
-  | GLetIn (loc,na,b,t,c) ->
+      GProd (na,bk,comp1,comp2)
+  | GLetIn (na,b,t,c) ->
       let comp1 = f b in
       let compt = Option.map f t in
       let comp2 = f c in
-      GLetIn (loc,na,comp1,compt,comp2)
-  | GCases (loc,sty,rtntypopt,tml,pl) ->
+      GLetIn (na,comp1,compt,comp2)
+  | GCases (sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
       let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
-      let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in
-      GCases (loc,sty,comp1,comp2,comp3)
-  | GLetTuple (loc,nal,(na,po),b,c) ->
+      let comp3 = Util.List.map_left (fun (loc,(idl,p,c)) -> (loc,(idl,p,f c))) pl in
+      GCases (sty,comp1,comp2,comp3)
+  | GLetTuple (nal,(na,po),b,c) ->
       let comp1 = Option.map f po in
       let comp2 = f b in
       let comp3 = f c in
-      GLetTuple (loc,nal,(na,comp1),comp2,comp3)
-  | GIf (loc,c,(na,po),b1,b2) ->
+      GLetTuple (nal,(na,comp1),comp2,comp3)
+  | GIf (c,(na,po),b1,b2) ->
       let comp1 = Option.map f po in
       let comp2 = f b1 in
       let comp3 = f b2 in
-      GIf (loc,f c,(na,comp1),comp2,comp3)
-  | GRec (loc,fk,idl,bl,tyl,bv) ->
+      GIf (f c,(na,comp1),comp2,comp3)
+  | GRec (fk,idl,bl,tyl,bv) ->
       let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in
       let comp2 = Array.map f tyl in
       let comp3 = Array.map f bv in
-      GRec (loc,fk,idl,comp1,comp2,comp3)
-  | GCast (loc,c,k) ->
+      GRec (fk,idl,comp1,comp2,comp3)
+  | GCast (c,k) ->
       let comp1 = f c in
       let comp2 = Miscops.map_cast_type f k in
-      GCast (loc,comp1,comp2)
+      GCast (comp1,comp2)
   | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
+  )
 
 let map_glob_constr = map_glob_constr_left_to_right
 
 let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
 
-let fold_glob_constr f acc = function
+let fold_glob_constr f acc = Loc.with_unloc (function
   | GVar _ -> acc
-  | GApp (_,c,args) -> List.fold_left f (f acc c) args
-  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) ->
+  | GApp (c,args) -> List.fold_left f (f acc c) args
+  | GLambda (_,_,b,c) | GProd (_,_,b,c) ->
     f (f acc b) c
-  | GLetIn (_,_,b,t,c) ->
+  | GLetIn (_,b,t,c) ->
     f (Option.fold_left f (f acc b) t) c
-  | GCases (_,_,rtntypopt,tml,pl) ->
-    let fold_pattern acc (_,idl,p,c) = f acc c in
+  | GCases (_,rtntypopt,tml,pl) ->
+    let fold_pattern acc (_,(idl,p,c)) = f acc c in
     List.fold_left fold_pattern
       (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml))
       pl
-  | GLetTuple (_,_,rtntyp,b,c) ->
+  | GLetTuple (_,rtntyp,b,c) ->
     f (f (fold_return_type f acc rtntyp) b) c
-  | GIf (_,c,rtntyp,b1,b2) ->
+  | GIf (c,rtntyp,b1,b2) ->
     f (f (f (fold_return_type f acc rtntyp) c) b1) b2
-  | GRec (_,_,_,bl,tyl,bv) ->
+  | GRec (_,_,bl,tyl,bv) ->
     let acc = Array.fold_left
       (List.fold_left (fun acc (na,k,bbd,bty) ->
 	f (Option.fold_left f acc bbd) bty)) acc bl in
     Array.fold_left f (Array.fold_left f acc tyl) bv
-  | GCast (_,c,k) ->
+  | GCast (c,k) ->
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
+  )
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
@@ -219,25 +221,25 @@ let same_id na id = match na with
 | Name id' -> Id.equal id id'
 
 let occur_glob_constr id =
-  let rec occur = function
-    | GVar (loc,id') -> Id.equal id id'
-    | GApp (loc,f,args) -> (occur f) || (List.exists occur args)
-    | GLambda (loc,na,bk,ty,c) ->
+  let rec occur gt = Loc.with_unloc (function
+    | GVar (id') -> Id.equal id id'
+    | GApp (f,args) -> (occur f) || (List.exists occur args)
+    | GLambda (na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
-    | GProd (loc,na,bk,ty,c) ->
+    | GProd (na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,t,c) ->
+    | GLetIn (na,b,t,c) ->
       (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
+    | GCases (sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         || (List.exists (fun (tm,_) -> occur tm) tml)
 	|| (List.exists occur_pattern pl)
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (nal,rtntyp,b,c) ->
 	occur_return_type rtntyp id
         || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c))
-    | GIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (c,rtntyp,b1,b2) ->
 	occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2)
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
+    | GRec (fk,idl,bl,tyl,bv) ->
         not (Array.for_all4 (fun fid bl ty bd ->
           let rec occur_fix = function
               [] -> not (occur ty) && (Id.equal fid id || not(occur bd))
@@ -249,11 +251,11 @@ let occur_glob_constr id =
                 (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) || (match k with CastConv t
+    | GCast (c,k) -> (occur c) || (match k with CastConv t
       | CastVM t | CastNative t -> occur t | CastCoerce -> false)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
-
-  and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c)
+    ) gt
+  and occur_pattern (loc,(idl,p,c)) = not (Id.List.mem id idl) && (occur c)
 
   and occur_option = function None -> false | Some p -> occur p
 
@@ -268,33 +270,33 @@ let add_name_to_ids set na =
     | Name id -> Id.Set.add id set
 
 let free_glob_vars =
-  let rec vars bounded vs = function
-    | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
-    | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
+  let rec vars bounded vs = Loc.with_unloc @@ (function
+    | GVar (id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
+    | GApp (f,args) -> List.fold_left (vars bounded) vs (f::args)
+    | GLambda (na,_,ty,c) | GProd (na,_,ty,c) ->
 	let vs' = vars bounded vs ty in
 	let bounded' = add_name_to_ids bounded na in
        vars bounded' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
+    | GLetIn (na,b,ty,c) ->
 	let vs' = vars bounded vs b in
 	let vs'' = Option.fold_left (vars bounded) vs' ty in
 	let bounded' = add_name_to_ids bounded na in
        vars bounded' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
+    | GCases (sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
 	List.fold_left (vars_pattern bounded) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (nal,rtntyp,b,c) ->
 	let vs1 = vars_return_type bounded vs rtntyp in
 	let vs2 = vars bounded vs1 b in
 	let bounded' = List.fold_left add_name_to_ids bounded nal in
 	vars bounded' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (c,rtntyp,b1,b2) ->
 	let vs1 = vars_return_type bounded vs rtntyp in
 	let vs2 = vars bounded vs1 c in
 	let vs3 = vars bounded vs2 b1 in
 	vars bounded vs3 b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
+    | GRec (fk,idl,bl,tyl,bv) ->
 	let bounded' = Array.fold_right Id.Set.add idl bounded in
 	let vars_fix i vs fid =
 	  let vs1,bounded1 =
@@ -312,11 +314,12 @@ let free_glob_vars =
 	  vars bounded1 vs2 bv.(i)
 	in
 	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bounded vs c in
+    | GCast (c,k) -> let v = vars bounded vs c in
 	(match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
+    )
 
-  and vars_pattern bounded vs (loc,idl,p,c) =
+  and vars_pattern bounded vs (loc,(idl,p,c)) =
     let bounded' = List.fold_right Id.Set.add idl bounded  in
     vars bounded' vs c
 
@@ -332,7 +335,7 @@ let free_glob_vars =
 
 let glob_visible_short_qualid c =
   let rec aux acc = function
-    | GRef (_,c,_) ->
+    | _, GRef (c,_) ->
         let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
         let dir,id = Libnames.repr_qualid  qualid in
         if DirPath.is_empty dir then id :: acc else acc
@@ -351,26 +354,26 @@ let add_and_check_ident id set =
   Id.Set.add id set
 
 let bound_glob_vars =
-  let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
+  let rec vars bound = Loc.with_loc (fun ~loc -> function
+    | GLambda (na,_,_,_) | GProd (na,_,_,_) | GLetIn (na,_,_,_) as c ->
         let bound = name_fold add_and_check_ident na bound in
-        fold_glob_constr vars bound c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
+        fold_glob_constr vars bound (loc, c)
+    | GCases (sty,rtntypopt,tml,pl) ->
 	let bound = vars_option bound rtntypopt in
 	let bound =
           List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in
 	List.fold_left vars_pattern bound pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (nal,rtntyp,b,c) ->
 	let bound = vars_return_type bound rtntyp in
 	let bound = vars bound b in
 	let bound = List.fold_right (name_fold add_and_check_ident) nal bound in
 	vars bound c
-    | GIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (c,rtntyp,b1,b2) ->
 	let bound = vars_return_type bound rtntyp in
 	let bound = vars bound c in
 	let bound = vars bound b1 in
 	vars bound b2
-    | GRec (loc,fk,idl,bl,tyl,bv) ->
+    | GRec (fk,idl,bl,tyl,bv) ->
 	let bound = Array.fold_right Id.Set.add idl bound in
 	let vars_fix i bound fid =
 	  let bound =
@@ -388,9 +391,10 @@ let bound_glob_vars =
 	in
 	Array.fold_left_i vars_fix bound idl
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound
-    | GApp _ | GCast _ as c -> fold_glob_constr vars bound c
+    | GApp _ | GCast _ as c -> fold_glob_constr vars bound (loc, c)
+    )
 
-  and vars_pattern bound (loc,idl,p,c) =
+  and vars_pattern bound (loc,(idl,p,c)) =
     let bound = List.fold_right add_and_check_ident idl bound in
     vars bound c
 
@@ -435,14 +439,14 @@ let rec map_case_pattern_binders f = Loc.map (function
       else PatCstr(c,rps,rna)
   )
 
-let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause =
+let map_cases_branch_binders f ((loc,(il,cll,rhs)) as x) : cases_clause =
   (* spiwack: not sure if I must do something with the list of idents.
      It is intended to be a superset of the free variable of the
      right-hand side, if I understand correctly. But I'm not sure when
      or how they are used. *)
   let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in
   if r == cll then x
-  else loc,il,r,rhs
+  else loc,(il,r,rhs)
 
 let map_pattern_binders f tomatch branches =
   CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch,
@@ -452,29 +456,14 @@ let map_pattern_binders f tomatch branches =
 
 let map_tomatch f (c,pp) : tomatch_tuple = f c , pp
 
-let map_cases_branch f (loc,il,cll,rhs) : cases_clause =
-  loc , il , cll , f rhs
+let map_cases_branch f (loc,(il,cll,rhs)) : cases_clause =
+  loc , (il , cll , f rhs)
 
 let map_pattern f tomatch branches =
   List.map (fun tm -> map_tomatch f tm) tomatch,
   List.map (fun br -> map_cases_branch f br) branches
 
-let loc_of_glob_constr = function
-  | GRef (loc,_,_) -> loc
-  | GVar (loc,_) -> loc
-  | GEvar (loc,_,_) -> loc
-  | GPatVar (loc,_) -> loc
-  | GApp (loc,_,_) -> loc
-  | GLambda (loc,_,_,_,_) -> loc
-  | GProd (loc,_,_,_,_) -> loc
-  | GLetIn (loc,_,_,_,_) -> loc
-  | GCases (loc,_,_,_,_) -> loc
-  | GLetTuple (loc,_,_,_,_) -> loc
-  | GIf (loc,_,_,_,_) -> loc
-  | GRec (loc,_,_,_,_,_) -> loc
-  | GSort (loc,_) -> loc
-  | GHole (loc,_,_,_) -> loc
-  | GCast (loc,_,_) -> loc
+let loc_of_glob_constr (loc, _) = loc
 
 (**********************************************************************)
 (* Alpha-renaming                                                     *)
@@ -506,73 +495,74 @@ let rename_var l id =
     if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
     else id
 
-let rec rename_glob_vars l = function
-  | GVar (loc,id) as r ->
+let rec rename_glob_vars l = Loc.map_with_loc (fun ~loc -> function
+  | GVar id as r ->
       let id' = rename_var l id in
-      if id == id' then r else GVar (loc,id')
-  | GRef (_,VarRef id,_) as r ->
+      if id == id' then r else GVar id'
+  | GRef (VarRef id,_) as r ->
       if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
       else r
-  | GProd (loc,na,bk,t,c) ->
+  | GProd (na,bk,t,c) ->
       let na',l' = update_subst na l in
-      GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLambda (loc,na,bk,t,c) ->
+      GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLambda (na,bk,t,c) ->
       let na',l' = update_subst na l in
-      GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLetIn (loc,na,b,t,c) ->
+      GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c)
+  | GLetIn (na,b,t,c) ->
       let na',l' = update_subst na l in
-      GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
+      GLetIn (na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
-  | GCases (loc,ci,po,tomatchl,cls) ->
+  | GCases (ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
         test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in
       let test_clause idl = List.iter (test_id l) idl in
       let po = Option.map (rename_glob_vars l) po in
       let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
-      let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in
-      GCases (loc,ci,po,tomatchl,cls)
-  | GLetTuple (loc,nal,(na,po),c,b) ->
+      let cls = Util.List.map_left (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(idl,p,rename_glob_vars l c))) cls in
+      GCases (ci,po,tomatchl,cls)
+  | GLetTuple (nal,(na,po),c,b) ->
      List.iter (test_na l) (na::nal);
-     GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po),
+     GLetTuple (nal,(na,Option.map (rename_glob_vars l) po),
                 rename_glob_vars l c,rename_glob_vars l b)
-  | GIf (loc,c,(na,po),b1,b2) ->
+  | GIf (c,(na,po),b1,b2) ->
      test_na l na;
-     GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
+     GIf (rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po),
           rename_glob_vars l b1,rename_glob_vars l b2)
-  | GRec (loc,k,idl,decls,bs,ts) ->
+  | GRec (k,idl,decls,bs,ts) ->
      Array.iter (test_id l) idl;
-     GRec (loc,k,idl,
+     GRec (k,idl,
            Array.map (List.map (fun (na,k,bbd,bty) ->
              test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
            Array.map (rename_glob_vars l) bs,
            Array.map (rename_glob_vars l) ts)
-  | r -> map_glob_constr (rename_glob_vars l) r
+  (* XXX: This located use case should be improved. *)
+  | r -> snd @@ map_glob_constr (rename_glob_vars l) (loc, r)
+  )
 
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
-let rec cases_pattern_of_glob_constr na = function
-  | GVar (loc,id) ->
+let rec cases_pattern_of_glob_constr na = Loc.map (function
+  | GVar id ->
     begin match na with
     | Name _ ->
       (* Unable to manage the presence of both an alias and a variable *)
       raise Not_found
-    | Anonymous -> Loc.tag ~loc @@ PatVar (Name id)
+    | Anonymous -> PatVar (Name id)
     end
-  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ PatVar na
-  | GRef (loc,ConstructRef cstr,_) ->
-      Loc.tag ~loc @@ PatCstr (cstr,[],na)
-  | GApp (loc,GRef (_,ConstructRef cstr,_),l) ->
-      Loc.tag ~loc @@ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+  | GHole (_,_,_) -> PatVar na
+  | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na)
+  | GApp ((_loc, GRef (ConstructRef cstr,_)),l) ->
+      PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
   | _ -> raise Not_found
+  )
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = Loc.with_loc (fun ~loc -> function
-  | PatCstr (cstr,[],Anonymous) ->
-      GRef (loc,ConstructRef cstr,None)
-  | PatCstr (cstr,l,Anonymous) ->
-      let ref = GRef (loc,ConstructRef cstr,None) in
-      GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
+let rec glob_constr_of_closed_cases_pattern_aux x = Loc.map_with_loc (fun ~loc -> function
+  | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
+  | PatCstr (cstr,l,Anonymous)  ->
+      let ref = Loc.tag ~loc @@ GRef (ConstructRef cstr,None) in
+      GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
   ) x
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 48ae93f3ef..6696e174bd 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,46 +324,46 @@ let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
     (fun () -> Pp.strbrk "Casts are ignored in patterns")
 
-let rec pat_of_raw metas vars = function
-  | GVar (_,id) ->
+let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
+  | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
-  | GPatVar (_,(false,n)) ->
+  | GPatVar (false,n) ->
       metas := n::!metas; PMeta (Some n)
-  | GRef (_,gr,_) ->
+  | GRef (gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp (_, GPatVar (_,(true,n)), cl) ->
+  | GApp ((_, GPatVar (true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | GApp (_,c,cl) ->
+  | GApp (c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | GLambda (_,na,bk,c1,c2) ->
+  | GLambda (na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GProd (_,na,bk,c1,c2) ->
+  | GProd (na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GLetIn (_,na,c1,t,c2) ->
+  | GLetIn (na,c1,t,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
-  | GSort (_,s) ->
+  | GSort s ->
       PSort s
   | GHole _ ->
       PMeta None
-  | GCast (_,c,_) ->
+  | GCast (c,_) ->
       warn_cast_in_pattern ();
       pat_of_raw metas vars c
-  | GIf (_,c,(_,None),b1,b2) ->
+  | GIf (c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
-  | GLetTuple (loc,nal,(_,None),b,c) ->
-      let mkGLambda c na =
-	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+  | GLetTuple (nal,(_,None),b,c) ->
+      let mkGLambda c na = Loc.tag ~loc @@
+	GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
@@ -374,9 +374,9 @@ let rec pat_of_raw metas vars = function
       let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
       PCase (cip, PMeta None, pat_of_raw metas vars b,
              [0,tags,pat_of_raw metas vars c])
-  | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
+  | GCases (sty,p,[c,(na,indnames)],brs) ->
       let get_ind = function
-	| (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind
+	| (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
@@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,(_,nal)) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-        | (None | Some (GHole _)), _ -> PMeta None
+        | (None | Some (_, GHole _)), _ -> PMeta None
 	| Some p, None ->
             user_err ~loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
@@ -404,7 +404,8 @@ let rec pat_of_raw metas vars = function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.")
+  | r -> err ~loc (Pp.str "Non supported pattern.")
+  )
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
@@ -415,8 +416,8 @@ and pats_of_glob_branches loc metas vars ind brs =
   in
   let rec get_pat indexes = function
     | [] -> false, []
-    | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
-    | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs ->
+    | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *)
+    | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs ->
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->
@@ -431,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs =
       let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
       let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
       ext, ((j-1, tags, pat) :: pats)
-    | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.")
+    | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ae87cd8c02..5f9f4bb08a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -567,23 +567,23 @@ let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) (loc, t) =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
   let pretype = pretype k0 resolve_tc in
   let open Context.Rel.Declaration in
   match t with
-  | GRef (loc,ref,u) ->
+  | GRef (ref,u) ->
       inh_conv_coerce_to_tycon loc env evdref
 	(pretype_ref loc evdref env ref u)
 	tycon
 
-  | GVar (loc, id) ->
+  | GVar id ->
     inh_conv_coerce_to_tycon loc env evdref
       (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
       tycon
 
-  | GEvar (loc, id, inst) ->
+  | GEvar (id, inst) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
 	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let evk =
@@ -596,7 +596,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
-  | GPatVar (loc,(someta,n)) ->
+  | GPatVar (someta,n) ->
     let env = ltac_interp_name_env k0 lvar env !evdref in
     let ty =
       match tycon with
@@ -605,7 +605,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let k = Evar_kinds.MatchingVar (someta,n) in
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
-  | GHole (loc, k, naming, None) ->
+  | GHole (k, naming, None) ->
       let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
@@ -614,7 +614,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
           new_type_evar env evdref loc in
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
-  | GHole (loc, k, _naming, Some arg) ->
+  | GHole (k, _naming, Some arg) ->
       let env = ltac_interp_name_env k0 lvar env !evdref in
       let ty =
         match tycon with
@@ -626,7 +626,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let () = evdref := sigma in
       { uj_val = c; uj_type = ty }
 
-  | GRec (loc,fixkind,names,bl,lar,vdef) ->
+  | GRec (fixkind,names,bl,lar,vdef) ->
     let rec type_bl env ctxt = function
     [] -> ctxt
       | (na,bk,None,ty)::bl ->
@@ -711,11 +711,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
-  | GSort (loc,s) ->
+  | GSort s ->
     let j = pretype_sort loc evdref s in
       inh_conv_coerce_to_tycon loc env evdref j tycon
 
-  | GApp (loc,f,args) ->
+  | GApp (f,args) ->
     let fj = pretype empty_tycon env evdref lvar f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
@@ -794,7 +794,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-  | GLambda(loc,name,bk,c1,c2)      ->
+  | GLambda(name,bk,c1,c2)      ->
     let tycon' = evd_comb1
       (fun evd tycon ->
 	match tycon with
@@ -816,7 +816,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-  | GProd(loc,name,bk,c1,c2)        ->
+  | GProd(name,bk,c1,c2)        ->
     let j = pretype_type empty_valcon env evdref lvar c1 in
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
@@ -840,7 +840,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         iraise (e, info) in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-  | GLetIn(loc,name,c1,t,c2)      ->
+  | GLetIn(name,c1,t,c2)      ->
     let tycon1 =
       match t with
       | Some t ->
@@ -861,7 +861,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
 
-  | GLetTuple (loc,nal,(na,po),c,d) ->
+  | GLetTuple (nal,(na,po),c,d) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
@@ -954,7 +954,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
-  | GIf (loc,c,(na,po),b1,b2) ->
+  | GIf (c,(na,po),b1,b2) ->
     let cj = pretype empty_tycon env evdref lvar c in
     let (IndType (indf,realargs)) =
       try find_rectype env.ExtraEnv.env !evdref cj.uj_type
@@ -1022,12 +1022,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let cj = { uj_val = v; uj_type = p } in
       inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-  | GCases (loc,sty,po,tml,eqns) ->
+  | GCases (sty,po,tml,eqns) ->
     Cases.compile_cases loc sty
       ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref)
       tycon env.ExtraEnv.env (* loc *) (po,tml,eqns)
 
-  | GCast (loc,c,k) ->
+  | GCast (c,k) ->
     let cj =
       match k with
       | CastCoerce ->
@@ -1097,7 +1097,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
 and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
-  | GHole (loc, knd, naming, None) ->
+  | loc, GHole (knd, naming, None) ->
       let rec is_Type c = match EConstr.kind !evdref c with
       | Sort s ->
         begin match ESorts.kind !evdref s with