[location] Switch glob_constr to Loc.located

5 files changed, 340 insertions, 317 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d45f3a9f1..bbc98dd28 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -157,7 +157,7 @@ let insert_pat_alias loc p = function
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let extern_evar loc n l = Loc.tag @@ CEvar (n,l)
+let extern_evar n l = CEvar (n,l)
 
 (** We allow customization of the global_reference printer.
     For instance, in the debugger the tables of global references
@@ -475,7 +475,7 @@ exception Expl
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize loc inctx impl (cf,f) args =
+let explicitize inctx impl (cf,f) args =
   let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
@@ -512,41 +512,41 @@ let explicitize loc inctx impl (cf,f) args =
 	let args1 = exprec 1 (args1,impl1) in
 	let args2 = exprec (i+1) (args2,impl2) in
 	let ip = Some (List.length args1) in
-	  Loc.tag ~loc @@ CApp ((ip,f),args1@args2)
+	  CApp ((ip,f),args1@args2)
     | None ->
       let args = exprec 1 (args,impl) in
-	if List.is_empty args then f else Loc.tag ~loc @@ CApp ((None, f), args)
+	if List.is_empty args then snd f else CApp ((None, f), args)
   in
     try expl ()
     with Expl -> 
-      let f',us = match f with _loc, CRef (f,us) -> f,us | _ -> assert false in
+      let f',us = match f with (_loc, CRef (f,us)) -> f,us | _ -> assert false in
       let ip = if !print_projections then ip else None in
-	Loc.tag ~loc @@ CAppExpl ((ip, f', us), List.map Lazy.force args)
+	CAppExpl ((ip, f', us), List.map Lazy.force args)
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
   | [] -> false
 
-let extern_global loc impl f us =
+let extern_global impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
-    Loc.tag ~loc @@ CAppExpl ((None, f, us), [])
+    CAppExpl ((None, f, us), [])
   else
-    Loc.tag ~loc @@ CRef (f,us)
+    CRef (f,us)
 
-let extern_app loc inctx impl (cf,f) us args =
+let extern_app inctx impl (cf,f) us args =
   if List.is_empty args then
     (* If coming from a notation "Notation a := @b" *)
-    Loc.tag ~loc @@ CAppExpl ((None, f, us), [])
+    CAppExpl ((None, f, us), [])
   else if not !Constrintern.parsing_explicit &&
     ((!Flags.raw_print ||
       (!print_implicits && not !print_implicits_explicit_args)) &&
      List.exists is_status_implicit impl)
   then
     let args = List.map Lazy.force args in
-    Loc.tag ~loc @@ CAppExpl ((is_projection (List.length args) cf,f,us), args)
+    CAppExpl ((is_projection (List.length args) cf,f,us), args)
   else
-    explicitize loc inctx impl (cf, Loc.tag ~loc @@ CRef (f,us)) args
+    explicitize inctx impl (cf, Loc.tag @@ CRef (f,us)) args
 
 let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
 | [], _ -> []
@@ -560,7 +560,7 @@ let extern_args extern env args =
   List.map map args
 
 let match_coercion_app = function
-  | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
+  | (loc, GApp ((_, GRef (r,_)),args)) -> Some (loc, r, 0, args)
   | _ -> None
 
 let rec remove_coercions inctx c =
@@ -582,13 +582,13 @@ let rec remove_coercions inctx c =
 		 been confused with ordinary application or would have need
                  a surrounding context and the coercion to funclass would
                  have been made explicit to match *)
-	      if List.is_empty l then a' else GApp (loc,a',l)
+	      if List.is_empty l then a' else Loc.tag ~loc @@ GApp (a',l)
 	  | _ -> c
       with Not_found -> c)
   | _ -> c
 
 let rec flatten_application = function
-  | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l))
+  | (loc, GApp ((_, GApp(a,l')),l)) -> flatten_application (Loc.tag ~loc @@ GApp (a,l'@l))
   | a -> a
 
 (**********************************************************************)
@@ -616,7 +616,7 @@ let extern_optimal_prim_token scopes r r' =
 
 let extended_glob_local_binder_of_decl loc = function
   | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t)
-  | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None)
+  | (p,bk,Some x,(_,GHole ( _, Misctypes.IntroAnonymous, None))) -> GLocalDef (loc,p,bk,x,None)
   | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t)
 
 (**********************************************************************)
@@ -642,25 +642,25 @@ let rec extern inctx scopes vars r =
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_notation scopes vars r'' (uninterp_notations r'')
-  with No_match -> match r' with
-  | GRef (loc,ref,us) ->
-      extern_global loc (select_stronger_impargs (implicits_of_global ref))
+  with No_match -> Loc.map_with_loc (fun ~loc -> function
+  | GRef (ref,us) ->
+      extern_global (select_stronger_impargs (implicits_of_global ref))
         (extern_reference loc vars ref) (extern_universes us)
 
-  | GVar (loc,id) -> Loc.tag ~loc @@ CRef (Ident (loc,id),None)
+  | GVar id -> CRef (Ident (loc,id),None)
 
-  | GEvar (loc,n,[]) when !print_meta_as_hole -> Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)
+  | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
 
-  | GEvar (loc,n,l) ->
-      extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
+  | GEvar (n,l) ->
+      extern_evar n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,(b,n)) -> Loc.tag ~loc @@
+  | GPatVar (b,n) ->
       if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
         if b then CPatVar n else CEvar (n,[])
 
-  | GApp (loc,f,args) ->
+  | GApp (f,args) ->
       (match f with
-	 | GRef (rloc,ref,us) ->
+	 | (rloc, GRef (ref,us)) ->
 	     let subscopes = find_arguments_scope ref in
 	     let args = fill_arg_scopes args subscopes (snd scopes) in
 	     begin
@@ -701,42 +701,42 @@ let rec extern inctx scopes vars r =
                                      let head = extern true scopes vars arg in
 				     ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
-		 Loc.tag ~loc @@ CRecord (List.rev (ip projs locals args []))
+		 CRecord (List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
                     let args = extern_args (extern true) vars args in
-		     extern_app loc inctx
+		     extern_app inctx
 		       (select_stronger_impargs (implicits_of_global ref))
 		       (Some ref,extern_reference rloc vars ref) (extern_universes us) args
 	     end
-	       
+
 	 | _       ->
-	   explicitize loc inctx [] (None,sub_extern false scopes vars f)
+	   explicitize inctx [] (None,sub_extern false scopes vars f)
              (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
 
-  | GLetIn (loc,na,b,t,c) ->
-      Loc.tag ~loc @@ CLetIn ((loc,na),sub_extern false scopes vars b,
+  | GLetIn (na,b,t,c) ->
+      CLetIn ((loc,na),sub_extern false scopes vars b,
               Option.map (extern_typ scopes vars) t,
               extern inctx scopes (add_vname vars na) c)
 
-  | GProd (loc,na,bk,t,c) ->
+  | GProd (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
       let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
-      Loc.tag ~loc @@ CProdN ([(Loc.ghost,na)::idl,Default bk,t],c)
+      CProdN ([(Loc.ghost,na)::idl,Default bk,t],c)
 
-  | GLambda (loc,na,bk,t,c) ->
+  | GLambda (na,bk,t,c) ->
       let t = extern_typ scopes vars t in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in
-      Loc.tag ~loc @@ CLambdaN ([(Loc.ghost,na)::idl,Default bk,t],c)
+      CLambdaN ([(Loc.ghost,na)::idl,Default bk,t],c)
 
-  | GCases (loc,sty,rtntypopt,tml,eqns) ->
+  | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
       List.fold_right (name_fold Id.Set.add)
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
                  let na' = match na,tm with
-                   | Anonymous, GVar (_, id) ->
+                   | Anonymous, (_, GVar id) ->
                       begin match rtntypopt with
                             | None -> None
                             | Some ntn ->
@@ -745,7 +745,7 @@ let rec extern inctx scopes vars r =
                                else None
                       end
                    | Anonymous, _ -> None
-                   | Name id, GVar (_,id') when Id.equal id id' -> None
+                   | Name id, (_, GVar id') when Id.equal id id' -> None
                    | Name _, _ -> Some (Loc.ghost,na) in
                  (sub_extern false scopes vars tm,
                   na',
@@ -757,22 +757,22 @@ let rec extern inctx scopes vars r =
                 tml
     in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
-    Loc.tag ~loc @@ CCases (sty,rtntypopt',tml,eqns)
+    CCases (sty,rtntypopt',tml,eqns)
 
-  | GLetTuple (loc,nal,(na,typopt),tm,b) ->
-      Loc.tag ~loc @@ CLetTuple (List.map (fun na -> (Loc.ghost,na)) nal,
+  | GLetTuple (nal,(na,typopt),tm,b) ->
+      CLetTuple (List.map (fun na -> (Loc.ghost,na)) nal,
         (Option.map (fun _ -> (Loc.ghost,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
-  | GIf (loc,c,(na,typopt),b1,b2) ->
-      Loc.tag ~loc @@ CIf (sub_extern false scopes vars c,
+  | GIf (c,(na,typopt),b1,b2) ->
+      CIf (sub_extern false scopes vars c,
         (Option.map (fun _ -> (Loc.ghost,na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
-  | GRec (loc,fk,idv,blv,tyv,bv) ->
+  | GRec (fk,idv,blv,tyv,bv) ->
       let vars' = Array.fold_right Id.Set.add idv vars in
       (match fk with
 	 | GFix (nv,n) ->
@@ -792,7 +792,7 @@ let rec extern inctx scopes vars r =
 		 ((Loc.ghost, fi), (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in
-	     Loc.tag ~loc @@ CFix ((loc,idv.(n)),Array.to_list listdecl)
+	     CFix ((loc,idv.(n)),Array.to_list listdecl)
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
@@ -803,15 +803,16 @@ let rec extern inctx scopes vars r =
 		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
-	     Loc.tag ~loc @@ CCoFix ((loc,idv.(n)),Array.to_list listdecl))
+	     CCoFix ((loc,idv.(n)),Array.to_list listdecl))
 
-  | GSort (loc,s) -> Loc.tag ~loc @@ CSort (extern_glob_sort s)
+  | GSort s -> CSort (extern_glob_sort s)
 
-  | GHole (loc,e,naming,_) -> Loc.tag ~loc @@ CHole (Some e, naming, None) (** TODO: extern tactics. *)
+  | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
 
-  | GCast (loc,c, c') ->
-      Loc.tag ~loc @@ CCast (sub_extern true scopes vars c,
+  | GCast (c, c') ->
+      CCast (sub_extern true scopes vars c,
 	     Miscops.map_cast_type (extern_typ scopes vars) c')
+  ) r'
 
 and extern_typ (_,scopes) =
   extern true (Notation.current_type_scope_name (),scopes)
@@ -867,7 +868,7 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) = extern_local_binder scopes vars l in
       (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
 
-and extern_eqn inctx scopes vars (loc,ids,pl,c) =
+and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
   Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
@@ -878,13 +879,13 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
       try
         if List.mem keyrule !print_non_active_notations then raise No_match;
 	(* Adjusts to the number of arguments expected by the notation *)
-	let (t,args,argsscopes,argsimpls) = match t,n with
-	  | GApp (_,f,args), Some n
+	let (t,args,argsscopes,argsimpls) = match snd t,n with
+	  | GApp (f,args), Some n
 	      when List.length args >= n ->
 	      let args1, args2 = List.chop n args in
               let subscopes, impls =
-                match f with
-                | GRef (_,ref,us) ->
+                match snd f with
+                | GRef (ref,us) ->
 	          let subscopes =
 		    try List.skipn n (find_arguments_scope ref)
                     with Failure _ -> [] in
@@ -896,15 +897,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
                   subscopes,impls
                 | _ ->
                   [], [] in
-	      (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)),
+	      (if Int.equal n 0 then f else Loc.tag @@ GApp (f,args1)),
 	      args2, subscopes, impls
-	  | GApp (_,(GRef (_,ref,us) as f),args), None ->
+	  | GApp ((_, GRef (ref,us) as f),args), None ->
 	      let subscopes = find_arguments_scope ref in
 	      let impls =
 		  select_impargs_size
 		    (List.length args) (implicits_of_global ref) in
 	      f, args, subscopes, impls
-	  | GRef (_,ref,us), Some 0 -> GApp (Loc.ghost,t,[]), [], [], []
+	  | GRef (ref,us), Some 0 -> Loc.tag @@ GApp (t,[]), [], [], []
           | _, None -> t, [], [], []
           | _ -> raise No_match in
 	(* Try matching ... *)
@@ -945,7 +946,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
 	else
 	  let args = fill_arg_scopes args argsscopes scopes in
 	  let args = extern_args (extern true) vars args in
-	  explicitize loc false argsimpls (None,e) args
+	  Loc.tag ~loc @@ explicitize false argsimpls (None,e) args
       with
 	  No_match -> extern_notation allscopes vars t rules
 
@@ -965,8 +966,6 @@ let extern_glob_type vars c =
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
 
-let loc = Loc.ghost (* for constr and pattern, locations are lost *)
-
 let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
@@ -1008,11 +1007,11 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
 
 let any_any_branch =
   (* | _ => _ *)
-  (loc,[],[Loc.tag ~loc @@ PatVar Anonymous],GHole (loc,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+  Loc.tag ([],[Loc.tag @@ PatVar Anonymous], Loc.tag @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
 
-let rec glob_of_pat env sigma = function
-  | PRef ref -> GRef (loc,ref,None)
-  | PVar id -> GVar (loc,id)
+let rec glob_of_pat env sigma pat = Loc.tag @@ match pat with
+  | PRef ref -> GRef (ref,None)
+  | PVar id  -> GVar id
   | PEvar (evk,l) ->
       let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
@@ -1020,36 +1019,36 @@ let rec glob_of_pat env sigma = function
       | None -> Id.of_string "__"
       | Some id -> id
       in
-      GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
+      GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
 	| Anonymous ->
 	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
-      GVar (loc,id)
-  | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (loc,(false,n))
-  | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
+      GVar id
+  | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
+  | PMeta (Some n) -> GPatVar (false,n)
+  | PProj (p,c) -> GApp (Loc.tag @@ GRef (ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
-      GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
+      GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (loc,GPatVar (loc,(true,n)),
+      GApp (Loc.tag @@ GPatVar (true,n),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
-      GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
+      GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
   | PLetIn (na,b,t,c) ->
-      GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
+      GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
               glob_of_pat (na::env) sigma c)
   | PLambda (na,t,c) ->
-      GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
+      GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
   | PIf (c,b1,b2) ->
-      GIf (loc, glob_of_pat env sigma c, (Anonymous,None),
+      GIf (glob_of_pat env sigma c, (Anonymous,None),
            glob_of_pat env sigma b1, glob_of_pat env sigma b2)
   | PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
       let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
-      GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b)
+      GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b)
   | PCase (info,p,tm,bl) ->
       let mat = match bl, info.cip_ind with
 	| [], _ -> []
@@ -1066,10 +1065,10 @@ let rec glob_of_pat env sigma = function
 	  return_type_of_predicate ind nargs (glob_of_pat env sigma p)
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
-      GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
-  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
-  | PSort s -> GSort (loc,s)
+      GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
+  | PFix f -> Loc.obj @@ Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
+  | PCoFix c -> Loc.obj @@ Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
+  | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f814205dc..cc7203ac0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -304,12 +304,12 @@ let reset_tmp_scope env = {env with tmp_scope = None}
 
 let rec it_mkGProd loc2 env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GProd (na, bk, t, body))
     | [] -> body
 
 let rec it_mkGLambda loc2 env body =
   match env with
-      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
+      (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GLambda (na, bk, t, body))
     | [] -> body
 
 (**********************************************************************)
@@ -322,14 +322,14 @@ let build_impls = function
 
 let impls_type_list ?(args = []) =
   let rec aux acc = function
-    |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |_, GProd (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
     |_ -> (Variable,[],List.append args (List.rev acc),[])
   in aux []
 
 let impls_term_list ?(args = []) =
   let rec aux acc = function
-    |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
-    |GRec (_, fix_kind, nas, args, tys, bds) ->
+    |_, GLambda (na,bk,_,c) -> aux ((build_impls bk na)::acc) c
+    |_, GRec (fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
 	 aux acc' bds.(nb)
@@ -346,12 +346,12 @@ let rec check_capture ty = function
       ()
 
 let locate_if_hole loc na = function
-  | GHole (_,_,naming,arg) ->
+  | _, GHole (_,naming,arg) ->
       (try match na with
 	| Name id -> glob_constr_of_notation_constr loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> GHole (loc, Evar_kinds.BinderType na, naming, arg))
+      with Not_found -> Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
@@ -397,7 +397,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
     env fvs in
   let bl = List.map
     (fun (id, loc) ->
-      (loc, (Name id, b, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+      (loc, (Name id, b, Loc.tag ~loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -458,7 +458,7 @@ let glob_local_binder_of_extended = function
   | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
   | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
   | GLocalDef (loc,na,bk,c,None) ->
-      let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
   | GLocalPattern (loc,_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
@@ -517,10 +517,12 @@ let intern_generalization intern env lvar loc bk ak c =
       in
 	if pi then
 	  (fun (id, loc') acc ->
-	    GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            Loc.tag ~loc:(Loc.merge loc' loc) @@
+	    GProd (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
 	else
 	  (fun (id, loc') acc ->
-	    GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            Loc.tag ~loc:(Loc.merge loc' loc) @@
+	    GLambda (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
       List.fold_right (fun (id, loc as lid) (env, acc) ->
 	let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
@@ -572,10 +574,10 @@ let make_letins =
     (fun a c ->
      match a with
      | LPLetIn (loc,(na,b,t)) ->
-         GLetIn(loc,na,b,t,c)
+       Loc.tag ~loc @@ GLetIn(na,b,t,c)
      | LPCases (loc,(cp,il),id) ->
-         let tt = (GVar(loc,id),(Name id,None)) in
-         GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+         let tt = (Loc.tag ~loc @@ GVar id, (Name id,None)) in
+         Loc.tag ~loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
 
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
@@ -660,7 +662,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let bindings = Id.Map.map mk_env terms in
         Some (Genintern.generic_substitute_notation bindings arg)
       in
-      GHole (loc, knd, naming, arg)
+      Loc.tag ~loc @@ GHole (knd, naming, arg)
     | NBinderList (x,y,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -678,22 +680,22 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
         let (loc,(na,bk,t)) = a in
-        GProd (loc,na,bk,t,e)
+        Loc.tag ~loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let (loc,(na,bk,t)) = a in
-        GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+        Loc.tag ~loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
-	GProd (loc,na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ~loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
     | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
         when Name.equal na na' ->
         let subinfos,na = traverse_binder subst avoid subinfos na in
-        let ty = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
-	GLambda (loc,na,Explicit,ty,aux subst' subinfos c')
+        let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+	Loc.tag ~loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
     | t ->
       glob_constr_of_notation_constr_with_binders loc
         (traverse_binder subst avoid) (aux subst') subinfos t
@@ -705,11 +707,12 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
       intern {env with tmp_scope = scopt;
                 scopes = subscopes @ env.scopes} a
     with Not_found ->
+    Loc.tag ~loc (
     try
-      GVar (loc, Id.Map.find id renaming)
+      GVar (Id.Map.find id renaming)
     with Not_found ->
       (* Happens for local notation joint with inductive/fixpoint defs *)
-      GVar (loc,id)
+      GVar id)
   in aux (terms,None,None) infos c
 
 let split_by_type ids =
@@ -744,7 +747,7 @@ let string_of_ty = function
   | Variable -> "var"
 
 let gvar (loc, id) us = match us with
-| None -> GVar (loc, id)
+| None -> Loc.tag ~loc @@ GVar id
 | Some _ ->
   user_err ~loc  (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
@@ -786,25 +789,25 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
 	let impls = implicits_of_global ref in
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
-	GRef (loc, ref, us), impls, scopes, []
+	Loc.tag ~loc @@ GRef (ref, us), impls, scopes, []
       with e when CErrors.noncritical e ->
 	(* [id] a goal variable *)
 	gvar (loc,id) us, [], [], []
 
 let find_appl_head_data c =
-  match c with
-  | GRef (loc,ref,_) as x -> 
+  match Loc.obj c with
+  | GRef (ref,_) ->
     let impls = implicits_of_global ref in
     let scopes = find_arguments_scope ref in
-      x, impls, scopes, []
-  | GApp (_,GRef (_,ref,_),l) as x
+      c, impls, scopes, []
+  | GApp ((_, GRef (ref,_)),l)
       when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
       let scopes = find_arguments_scope ref in
-	x, List.map (drop_first_implicits n) impls,
+	c, List.map (drop_first_implicits n) impls,
 	List.skipn_at_least n scopes,[]
-  | x -> x,[],[],[]
+  | _ -> c,[],[],[]
 
 let error_not_enough_arguments loc =
   user_err ~loc  (str "Abbreviation is not applied enough.")
@@ -836,7 +839,7 @@ let intern_reference ref =
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env lvar us args =
   match intern_extended_global_of_qualid (loc,qid) with
-  | TrueGlobal ref -> GRef (loc, ref, us), true, args
+  | TrueGlobal ref -> (Loc.tag ~loc @@ GRef (ref, us)), true, args
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
@@ -850,9 +853,9 @@ let intern_qualid loc qid intern env lvar us args =
       let c = instantiate_notation_constr loc intern lvar subst infos c in
       let c = match us, c with
       | None, _ -> c
-      | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us)
-      | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
-         GApp (loc, GRef (loc', ref, us), arg)
+      | Some _, (loc, GRef (ref, None)) -> Loc.tag ~loc @@ GRef (ref, us)
+      | Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) ->
+        Loc.tag ~loc @@ GApp (Loc.tag ~loc:loc' @@ GRef (ref, us), arg)
       | Some _, _ ->
         user_err ~loc  (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
@@ -863,7 +866,7 @@ let intern_qualid loc qid intern env lvar us args =
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env lvar us args =
   match intern_qualid loc qid intern env lvar us args with
-    | GRef (_, VarRef _, _),_,_ -> raise Not_found
+    | (_, GRef (VarRef _, _)),_,_ -> raise Not_found
     | r -> r
 
 let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
@@ -1470,8 +1473,8 @@ let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
 let set_hole_implicit i b = function
-  | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
-  | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+  | (loc, GVar id) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
 let exists_implicit_name id =
@@ -1558,7 +1561,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
-	GRec (loc,GFix
+	Loc.tag ~loc @@
+          GRec (GFix
 	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
               Array.map (fun (_,bl,_,_) -> bl) idl,
@@ -1584,7 +1588,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
 					    en (Loc.ghost, Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
-	GRec (loc,GCoFix n,
+	Loc.tag ~loc @@
+	GRec (GCoFix n,
               Array.of_list lf,
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
@@ -1600,7 +1605,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
-	GLetIn (loc, snd na, inc1, int,
+	Loc.tag ~loc @@
+	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
@@ -1622,7 +1628,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    lvar us args ref 
 	in
 	  (* Rem: GApp(_,f,[]) stands for @f *)
-	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
+	Loc.tag ~loc @@
+	  GApp (f, intern_args env args_scopes (List.map fst args))
 
     | CApp ((isproj,f), args) ->
         let f,args = match f with
@@ -1687,20 +1694,21 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
              (* Build a return predicate by expansion of the patterns of the "in" clause *)
              let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
-             let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
-             let main_sub_eqn =
-               (Loc.ghost,[],thepats, (* "|p1,..,pn" *)
+             let sub_tms = List.map (fun id -> (Loc.tag @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+             let main_sub_eqn = Loc.tag @@
+               ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
-                  (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+                  (Loc.tag ~loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                 [Loc.ghost,[],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
-		  GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)]   (* "=> _" *) in
-             Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+                  [Loc.tag @@ ([],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
+                   Loc.tag @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
+             Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
-	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
+	Loc.tag ~loc @@
+	GCases (sty, rtnpo, tms, List.flatten eqns')
     | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
@@ -1709,7 +1717,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
 	  intern_type env'' u) po in
-        GLetTuple (loc, List.map snd nal, (na', p'), b',
+	Loc.tag ~loc @@
+        GLetTuple (List.map snd nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
@@ -1718,7 +1727,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
-        GIf (loc, c', (na', p'), intern env b1, intern env b2)
+	Loc.tag ~loc @@
+        GIf (c', (na', p'), intern env b1, intern env b2)
     | CHole (k, naming, solve) ->
         let k = match k with
         | None ->
@@ -1743,23 +1753,29 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
           let (_, glb) = Genintern.generic_intern ist gen in
           Some glb
         in
-	GHole (loc, k, naming, solve)
+	Loc.tag ~loc @@
+	GHole (k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar n when allow_patvar ->
-	GPatVar (loc, (true,n))
+	Loc.tag ~loc @@
+	GPatVar (true,n)
     | CEvar (n, []) when allow_patvar ->
-	GPatVar (loc, (false,n))
+	Loc.tag ~loc @@
+	GPatVar (false,n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (n, l) ->
-	GEvar (loc, n, List.map (on_snd (intern env)) l)
+	Loc.tag ~loc @@
+	GEvar (n, List.map (on_snd (intern env)) l)
     | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
     | CSort s ->
-	GSort(loc,s)
+	Loc.tag ~loc @@
+	GSort s
     | CCast (c1, c2) ->
-        GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
+	Loc.tag ~loc @@
+        GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
   )
   and intern_type env = intern (set_type_scope env)
 
@@ -1790,15 +1806,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       let rhs' = intern {env with ids = env_ids} rhs in
-      (loc,eqn_ids,pl,rhs')) pll
+      (loc,(eqn_ids,pl,rhs'))) pll
 
   and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (* the "match" part *)
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
-      | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id)
+      | (loc , GVar id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
+      | (loc, GRef (VarRef id, _)), None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
@@ -1870,8 +1886,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-	    GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
-	      aux (n+1) impl' subscopes' eargs rargs
+              (Loc.map (fun (a,b,c) -> GHole(a,b,c))
+                (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c)
+              ) :: aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
 	  intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
@@ -1895,8 +1912,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   and smart_gapp f loc = function
     | [] -> f
     | l -> match f with
-      | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l)
-      | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l)
+      | (loc', GApp (g, args)) -> Loc.tag ~loc:(Loc.merge loc' loc) @@ GApp (g, args@l)
+      | _ -> Loc.tag ~loc:(Loc.merge (loc_of_glob_constr f) loc) @@ GApp (f, l)
 
   and intern_args env subscopes = function
     | [] -> []
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d2bebfb54..51152bb24 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -125,37 +125,38 @@ let add_name_to_ids set na =
   | Name id -> Id.Set.add id set
 
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
-  let rec vars bound vs = function
-    | GVar (loc,id) ->
+  let rec vars bound vs (loc, t) = match t with
+    | GVar id ->
 	if is_freevar bound (Global.env ()) id then
 	  if Id.List.mem_assoc id vs then vs
 	  else (id, loc) :: vs
 	else vs
-    | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
+
+    | GApp (f,args) -> List.fold_left (vars bound) vs (f::args)
+    | GLambda (na,_,ty,c) | GProd (na,_,ty,c) ->
 	let vs' = vars bound vs ty in
 	let bound' = add_name_to_ids bound na in
 	vars bound' vs' c
-    | GLetIn (loc,na,b,ty,c) ->
+    | GLetIn (na,b,ty,c) ->
 	let vs' = vars bound vs b in
 	let vs'' = Option.fold_left (vars bound) vs' ty in
 	let bound' = add_name_to_ids bound na in
 	vars bound' vs'' c
-    | GCases (loc,sty,rtntypopt,tml,pl) ->
+    | GCases (sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bound vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
 	List.fold_left (vars_pattern bound) vs2 pl
-    | GLetTuple (loc,nal,rtntyp,b,c) ->
+    | GLetTuple (nal,rtntyp,b,c) ->
 	let vs1 = vars_return_type bound vs rtntyp in
 	let vs2 = vars bound vs1 b in
 	let bound' = List.fold_left add_name_to_ids bound nal in
 	vars bound' vs2 c
-    | GIf (loc,c,rtntyp,b1,b2) ->
+    | GIf (c,rtntyp,b1,b2) ->
 	let vs1 = vars_return_type bound vs rtntyp in
 	let vs2 = vars bound vs1 c in
 	let vs3 = vars bound vs2 b1 in
 	vars bound vs3 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 vs fid =
 	  let vs1,bound1 =
@@ -173,11 +174,11 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  vars bound1 vs2 bv.(i)
 	in
 	Array.fold_left_i vars_fix vs idl
-    | GCast (loc,c,k) -> let v = vars bound vs c in
+    | GCast (c,k) -> let v = vars bound vs c in
 	(match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
-  and vars_pattern bound vs (loc,idl,p,c) =
+  and vars_pattern bound vs (loc,(idl,p,c)) =
     let bound' = List.fold_right Id.Set.add idl bound  in
     vars bound' vs c
 
@@ -309,12 +310,12 @@ let implicits_of_glob_constr ?(with_products=true) l =
     (ExplByPos (i, name), (true, true, true)) :: l
   | _ -> l
   in
-  let rec aux i c =
+  let rec aux i (loc, c) =
     let abs na bk b =
       add_impl i na bk (aux (succ i) b)
     in
       match c with
-      | GProd (loc, na, bk, t, b) ->
+      | GProd (na, bk, t, b) ->
 	  if with_products then abs na bk b
 	  else
             let () = match bk with
@@ -323,9 +324,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
 			      pr_name na ++ strbrk " and following binders")
             | _ -> ()
             in []
-      | GLambda (loc, na, bk, t, b) -> abs na bk b
-      | GLetIn (loc, na, b, t, c) -> aux i c
-      | GRec (_, fix_kind, nas, args, tys, bds) ->
+      | GLambda (na, bk, t, b) -> abs na bk b
+      | GLetIn (na, b, t, c) -> aux i b
+      | GRec (fix_kind, nas, args, tys, bds) ->
        let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
        List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
       | _ -> []
diff --git a/interp/notation.ml b/interp/notation.ml
index aef089299..3bcec3001 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -264,12 +264,12 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
 let prim_token_key_table = ref KeyMap.empty
 
 let glob_prim_constr_key = function
-  | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref)
+  | _, GApp ((_, GRef (ref,_)),_) | _, GRef (ref,_) -> RefKey (canonical_gr ref)
   | _ -> Oth
 
 let glob_constr_keys = function
-  | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth]
-  | GRef (_,ref,_) -> [RefKey (canonical_gr ref)]
+  | _, GApp ((_, GRef (ref,_)),_) -> [RefKey (canonical_gr ref); Oth]
+  | _, GRef (ref,_) -> [RefKey (canonical_gr ref)]
   | _ -> [Oth]
 
 let cases_pattern_key = function
@@ -471,13 +471,14 @@ let interp_prim_token =
 
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
-let rec rcp_of_glob looked_for = function
-  | GVar (loc,id)     -> Loc.tag ~loc @@ RCPatAtom (Some id)
-  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None)
-  | GRef (loc,g,_)    -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[])
-  | GApp (loc,GRef (_,g,_),l) ->
-    looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
+let rec rcp_of_glob looked_for gt = Loc.map (function
+  | GVar id       -> RCPatAtom (Some id)
+  | GHole (_,_,_) -> RCPatAtom None
+  | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
+  | GApp ((_, GRef (g,_)),l) ->
+    looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
   | _ -> raise Not_found
+  ) gt
 
 let interp_prim_token_cases_pattern_expr loc looked_for p =
   interp_prim_token_gen (rcp_of_glob looked_for) loc p
@@ -521,8 +522,8 @@ let uninterp_prim_token_ind_pattern ind args =
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
-    let ref = GRef (Loc.ghost,ref,None) in
-    match numpr (GApp (Loc.ghost,ref,args')) with
+    let ref = Loc.tag @@ GRef (ref,None) in
+    match numpr (Loc.tag @@ GApp (ref,args')) with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
   with Not_found -> raise Notation_ops.No_match
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a25fd81f3..32c900504 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -24,19 +24,19 @@ open Notation_term
 
 let on_true_do b f c = if b then (f c; b) else b
 
-let compare_glob_constr f add t1 t2 = match t1,t2 with
-  | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
-  | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
-  | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
-  | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
+let compare_glob_constr f add (_l1, t1) (_l2, t2) = match t1,t2 with
+  | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2
+  | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1)
+  | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
+  | GLambda (na1,bk1,ty1,c1), GLambda (na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 && f c1 c2) add na1
-  | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
+  | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
       on_true_do (f ty1 ty2 && f c1 c2) add na1
   | GHole _, GHole _ -> true
-  | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
-  | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 ->
+  | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+  | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 ->
       on_true_do (f b1 b2 && f c1 c2) add na1
   | (GCases _ | GRec _
     | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
@@ -129,49 +129,51 @@ let rec cases_pattern_fold_map loc g e = Loc.with_unloc (function
 let subst_binder_type_vars l = function
   | Evar_kinds.BinderType (Name id) ->
      let id =
-       try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+       try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id
        with Not_found -> id in
      Evar_kinds.BinderType (Name id)
   | e -> e
 
-let rec subst_glob_vars l = function
-  | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
-  | GProd (loc,Name id,bk,t,c) ->
+let rec subst_glob_vars l gc = Loc.map (function
+  | GVar id as r -> (try snd @@ Id.List.assoc id l with Not_found -> r)
+  | GProd (Name id,bk,t,c) ->
       let id =
-	try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+	try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id
 	with Not_found -> id in
-      GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
-  | GLambda (loc,Name id,bk,t,c) ->
+      GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+  | GLambda (Name id,bk,t,c) ->
       let id =
-	try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+	try match snd @@ Id.List.assoc id l with GVar id' -> id' | _ -> id
 	with Not_found -> id in
-      GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
-  | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg)
-  | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
+      GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+  | GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg)
+  | _ -> snd @@ map_glob_constr (subst_glob_vars l) gc (* assume: id is not binding *)
+  ) gc
 
 let ldots_var = Id.of_string ".."
 
-let glob_constr_of_notation_constr_with_binders loc g f e = function
-  | NVar id -> GVar (loc,id)
-  | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
+let glob_constr_of_notation_constr_with_binders loc g f e nc =
+  let lt x = Loc.tag ~loc x in lt @@ match nc with
+  | NVar id -> GVar id
+  | NApp (a,args) -> GApp (f e a, List.map (f e) args)
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
-      let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
-      let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
-      let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in
-      subst_glob_vars outerl it
+      let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+      let inner  = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
+      let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+      Loc.obj @@ subst_glob_vars outerl it
   | NBinderList (x,y,iter,tail) ->
       let t = f e tail in let it = f e iter in
-      let innerl = [(ldots_var,t);(x,GVar(loc,y))] in
-      let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
+      let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in
+      let inner  = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
       let outerl = [(ldots_var,inner)] in
-      subst_glob_vars outerl it
+      Loc.obj @@ subst_glob_vars outerl it
   | NLambda (na,ty,c) ->
-      let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c)
+      let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
   | NProd (na,ty,c) ->
-      let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c)
+      let e',na = g e na in GProd (na,Explicit,f e ty,f e' c)
   | NLetIn (na,b,t,c) ->
-      let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c)
+      let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c)
   | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -186,25 +188,25 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
-	(loc,idl,patl,f e rhs)) eqnl in
-      GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
+	lt (idl,patl,f e rhs)) eqnl in
+      GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
       let e',nal = List.fold_map g e nal in
       let e'',na = g e na in
-      GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
+      GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
   | NIf (c,(na,po),b1,b2) ->
       let e',na = g e na in
-      GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
+      GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
       let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = Array.fold_map (to_id g) e idl in
-      GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
-  | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
-  | NSort x -> GSort (loc,x)
-  | NHole (x, naming, arg)  -> GHole (loc, x, naming, arg)
-  | NRef x -> GRef (loc,x,None)
+      GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
+  | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
+  | NSort x -> GSort x
+  | NHole (x, naming, arg)  -> GHole (x, naming, arg)
+  | NRef x -> GRef (x,None)
 
 let glob_constr_of_notation_constr loc x =
   let rec aux () x =
@@ -220,13 +222,13 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id
 let split_at_recursive_part c =
   let sub = ref None in
   let rec aux = function
-  | GApp (loc0,GVar(loc,v),c::l) when Id.equal v ldots_var ->
+  | loc0, GApp ((loc,GVar v),c::l) when Id.equal v ldots_var ->
       begin match !sub with
       | None ->
         let () = sub := Some c in
         begin match l with
-        | [] -> GVar (loc, ldots_var)
-        | _ :: _ -> GApp (loc0, GVar (loc, ldots_var), l)
+        | []     -> Loc.tag ~loc @@ GVar ldots_var
+        | _ :: _ -> Loc.tag ~loc:loc0 @@ GApp (Loc.tag ~loc @@ GVar ldots_var, l)
         end
       | Some _ ->
         (* Not narrowed enough to find only one recursive part *)
@@ -237,13 +239,13 @@ let split_at_recursive_part c =
   match !sub with
   | None -> (* No recursive pattern found *) raise Not_found
   | Some c ->
-  match outer_iterator with
-  | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
+  match Loc.obj outer_iterator with
+  | GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
   | _ -> outer_iterator, c
 
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
-let check_is_hole id = function GHole _ -> () | t ->
+let check_is_hole id = function _, GHole _ -> () | t ->
   user_err ~loc:(loc_of_glob_constr t)
    (strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
@@ -257,19 +259,19 @@ type recursive_pattern_kind =
 let compare_recursive_parts found f f' (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
-  let rec aux c1 c2 = match c1,c2 with
-  | GVar(_,v), term when Id.equal v ldots_var ->
+  let rec aux (l1, c1) (l2, c2) = match c1, c2 with
+  | GVar v, term when Id.equal v ldots_var ->
       (* We found the pattern *)
       assert (match !terminator with None -> true | Some _ -> false);
-      terminator := Some term;
+      terminator := Some (l2, term);
       true
-  | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when Id.equal v ldots_var ->
+  | GApp ((_, GVar v),l1), GApp (term, l2) when Id.equal v ldots_var ->
       (* We found the pattern, but there are extra arguments *)
       (* (this allows e.g. alternative (recursive) notation of application) *)
       assert (match !terminator with None -> true | Some _ -> false);
       terminator := Some term;
       List.for_all2eq aux l1 l2
-  | GVar (_,x), GVar (_,y) when not (Id.equal x y) ->
+  | GVar x, GVar y when not (Id.equal x y) ->
       (* We found the position where it differs *)
       let lassoc = match !terminator with None -> false | Some _ -> true in
       let x,y = if lassoc then y,x else x,y in
@@ -279,8 +281,8 @@ let compare_recursive_parts found f f' (iterator,subc) =
         true
       | Some _ -> false
       end
-  | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
-  | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
+  | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
+  | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) ->
       (* We found a binding position where it differs *)
       begin match !diff with
       | None ->
@@ -289,7 +291,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
       | Some _ -> false
       end
   | _ ->
-      compare_glob_constr aux (add_name found) c1 c2 in
+      compare_glob_constr aux (add_name found) (l1, c1) (l2, c2) in
   if aux iterator subc then
     match !diff with
     | None ->
@@ -312,13 +314,13 @@ let compare_recursive_parts found f f' (iterator,subc) =
             (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
 	let iterator =
 	  f' (if lassoc then iterator
-	      else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
+	      else subst_glob_vars [x, Loc.tag @@ GVar y] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,RecursiveBinders (t_x,t_y)) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
-	let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
+	let iterator = f' (subst_glob_vars [x, Loc.tag @@ GVar y] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	check_is_hole x t_x;
@@ -336,22 +338,22 @@ let notation_constr_and_vars_of_glob_constr a =
     try compare_recursive_parts found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
-    match c with
-    | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var ->
+    match snd c with
+    | GApp ((loc, GVar f),[c]) when Id.equal f ldots_var ->
 	(* Fall on the second part of the recursive pattern w/o having
 	   found the first part *)
 	user_err ~loc 
 	(str "Cannot find where the recursive pattern starts.")
-    | c ->
+    | _c ->
 	aux' c
-  and aux' = function
-  | GVar (_,id) -> add_id found id; NVar id
-  | GApp (_,g,args) -> NApp (aux g, List.map aux args)
-  | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
-  | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
-  | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c)
-  | GCases (_,sty,rtntypopt,tml,eqnl) ->
-      let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
+  and aux' x = Loc.with_unloc (function
+  | GVar id -> add_id found id; NVar id
+  | GApp (g,args) -> NApp (aux g, List.map aux args)
+  | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
+  | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
+  | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
+  | GCases (sty,rtntypopt,tml,eqnl) ->
+      let f (_,(idl,pat,rhs)) = List.iter (add_id found) idl; (pat,aux rhs) in
       NCases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
@@ -359,29 +361,29 @@ let notation_constr_and_vars_of_glob_constr a =
 	    (fun (_,(_,nl)) -> List.iter (add_name found) nl) x;
           (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml,
         List.map f eqnl)
-  | GLetTuple (loc,nal,(na,po),b,c) ->
+  | GLetTuple (nal,(na,po),b,c) ->
       add_name found na;
       List.iter (add_name found) nal;
       NLetTuple (nal,(na,Option.map aux po),aux b,aux c)
-  | GIf (loc,c,(na,po),b1,b2) ->
+  | GIf (c,(na,po),b1,b2) ->
       add_name found na;
       NIf (aux c,(na,Option.map aux po),aux b1,aux b2)
-  | GRec (_,fk,idl,dll,tl,bl) ->
+  | GRec (fk,idl,dll,tl,bl) ->
       Array.iter (add_id found) idl;
       let dll = Array.map (List.map (fun (na,bk,oc,b) ->
 	 if bk != Explicit then
 	   error "Binders marked as implicit not allowed in notations.";
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
-  | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
-  | GSort (_,s) -> NSort s
-  | GHole (_,w,naming,arg) ->
+  | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+  | GSort s -> NSort s
+  | GHole (w,naming,arg) ->
      if arg != None then has_ltac := true;
      NHole (w, naming, arg)
-  | GRef (_,r,_) -> NRef r
+  | GRef (r,_) -> NRef r
   | GEvar _ | GPatVar _ ->
       error "Existential variables not allowed in notations."
-
+  ) x
   in
   let t = aux a in
   (* Side effect *)
@@ -590,8 +592,8 @@ let abstract_return_type_context pi mklam tml rtno =
 
 let abstract_return_type_context_glob_constr =
   abstract_return_type_context (fun (_,(_,nal)) -> nal)
-    (fun na c ->
-      GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
+    (fun na c -> Loc.tag @@
+      GLambda(na,Explicit,Loc.tag @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
 
 let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
@@ -663,18 +665,19 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
 let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
   (terms,onlybinders,termlists,(x,bl)::binderlists)
 
-let rec pat_binder_of_term = function
-  | GVar (loc, id) -> Loc.tag ~loc @@ PatVar (Name id)
-  | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
+let rec pat_binder_of_term t = Loc.map (function
+  | GVar id -> PatVar (Name id)
+  | GApp ((_, GRef (ConstructRef cstr,_)), l) ->
      let nparams = Inductiveops.inductive_nparams (fst cstr) in
      let _,l = List.chop nparams l in
-     Loc.tag ~loc @@ PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
+     PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
   | _ -> raise No_match
+  ) t
 
 let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
     let v' = Id.List.assoc var terms in
-    match v, v' with
+    match Loc.obj v, Loc.obj v' with
     | GHole _, _ -> sigma
     | _, GHole _ ->
         let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
@@ -688,7 +691,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
   try
     let vl' = Id.List.assoc var termlists in
     let unify_term v v' =
-      match v, v' with
+      match Loc.obj v, Loc.obj v' with
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
@@ -704,8 +707,8 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
 
 let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
-    match Id.List.assoc var terms with
-    | GVar (_,id') ->
+    match Loc.obj @@ Id.List.assoc var terms with
+    | GVar id' ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
     | _ -> anomaly (str "A term which can be a binder has to be a variable")
@@ -713,7 +716,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
     (* The matching against a term allowing to find the instance has not been found yet *)
     (* If it will be a different name, we shall unfortunately fail *)
     (* TODO: look at the consequences for alp *)
-    alp, add_env alp sigma var (GVar (Loc.ghost,id))
+    alp, add_env alp sigma var (Loc.tag @@ GVar id)
 
 let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
@@ -782,7 +785,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
     let unify_pat alp p p' =
       try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
     let unify_term alp v v' =
-      match v, v' with
+      match Loc.obj v, Loc.obj v' with
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
@@ -831,7 +834,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
       else raise No_match in
     let unify_term_binder c b' =
       match c, b' with
-      | GVar (loc, id), GLocalAssum (_, na', bk', t') ->
+      | (_, GVar id), GLocalAssum (loc, na', bk', t') ->
          GLocalAssum (loc, unify_id id na', bk', t')
       | c, GLocalPattern (loc, (p',ids), id, bk', t') ->
          let p = pat_binder_of_term c in
@@ -892,21 +895,22 @@ let rec match_cases_pattern_binders metas acc (_, pat1) (_, pat2) =
 
 let glue_letin_with_decls = true
 
-let rec match_iterated_binders islambda decls = function
-  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
+let rec match_iterated_binders islambda decls bi = Loc.with_loc (fun ~loc -> function
+  | GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))])))
       when islambda && Id.equal p e ->
-      match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
-  | GLambda (loc,na,bk,t,b) when islambda ->
-      match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
-  | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
+      match_iterated_binders islambda (GLocalPattern(loc,(cp,ids),p,bk,t)::decls) b
+  | GLambda (na,bk,t,b) when islambda ->
+      match_iterated_binders islambda (GLocalAssum(loc,na,bk,t)::decls) b
+  | GProd (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))])))
       when not islambda && Id.equal p e ->
-      match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
-  | GProd (loc,(Name _ as na),bk,t,b) when not islambda ->
-      match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
-  | GLetIn (loc,na,c,t,b) when glue_letin_with_decls ->
+      match_iterated_binders islambda (GLocalPattern(loc,(cp,ids),p,bk,t)::decls) b
+  | GProd ((Name _ as na),bk,t,b) when not islambda ->
+      match_iterated_binders islambda (GLocalAssum(loc,na,bk,t)::decls) b
+  | GLetIn (na,c,t,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
 	(GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b
-  | b -> (decls,b)
+  | b -> (decls, Loc.tag ~loc b)
+  ) bi
 
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
   (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
@@ -967,91 +971,92 @@ let does_not_come_from_already_eta_expanded_var =
   (* The following test is then an approximation of what can be done *)
   (* optimally (whether other looping situations can occur remains to be *)
   (* checked). *)
-  function GVar _ -> false | _ -> true
+  function _loc, GVar _ -> false | _ -> true
 
 let rec match_ inner u alp metas sigma a1 a2 =
-  match (a1,a2) with
+  let loc, a1_val = Loc.to_pair a1 in
+  match a1_val, a2 with
 
   (* Matching notation variable *)
-  | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
-  | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
-  | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
+  | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
+  | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+  | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
 
   (* Matching recursive notations for terms *)
   | r1, NList (x,y,iter,termin,lassoc) ->
-      match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
+      match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
 
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+  | GLambda (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
     NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
       let (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+  | GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
       let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+  | GProd (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
     NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
       let (decls,b) = match_iterated_binders true [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
 
-  | GProd (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
+  | GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
       when na1 != Anonymous ->
       let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
   (* Matching recursive notations for binders: general case *)
-  | r, NBinderList (x,y,iter,termin) ->
-      match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
+  | _r, NBinderList (x,y,iter,termin) ->
+      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+  | GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
     NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
       let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,b2)
+  | GLambda (na,bk,t,b1), NLambda (Name id,_,b2)
       when is_bindinglist_meta id metas ->
       let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
-  | GProd (loc,na,bk,t,b1), NProd (Name id,_,b2)
+  | GProd (na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
       let alp,sigma = bind_bindinglist_env alp sigma id [GLocalAssum (loc,na,bk,t)] in
       match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
-  | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
-  | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
-  | GApp (loc,f1,l1), NApp (f2,l2) ->
+  | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
+  | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+  | GApp (f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
 	if n1 < n2 then
 	  let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
 	else if n1 > n2 then
-	  let l11,l12 = List.chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
+	  let l11,l12 = List.chop (n1-n2) l1 in Loc.tag ~loc @@ GApp (f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
-  | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) ->
+  | GLambda (na1,_,t1,b1), NLambda (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) ->
+  | GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2)
-  | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
+  | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
+  | GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
-  | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
+  | GLetIn (na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
      match_binders u alp metas na1 na2
        (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
-  | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
+  | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
       when sty1 == sty2
 	 && Int.equal (List.length tml1) (List.length tml2)
 	 && Int.equal (List.length eqnl1) (List.length eqnl2) ->
@@ -1065,17 +1070,17 @@ let rec match_ inner u alp metas sigma a1 a2 =
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
       List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
-  | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
+  | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when Int.equal (List.length nal1) (List.length nal2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
       let sigma = match_in u alp metas sigma b1 b2 in
       let (alp,sigma) =
 	List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
       match_in u alp metas sigma c1 c2
-  | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
+  | GIf (a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
       List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
-  | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
+  | GRec (fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
       when match_fix_kind fk1 fk2 && Int.equal (Array.length idl1) (Array.length idl2) &&
 	Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2
 	->
@@ -1089,13 +1094,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2)
-  | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) ->
+  | GCast(c1,CastConv t1), NCast (c2,CastConv t2)
+  | GCast(c1,CastVM t1), NCast (c2,CastVM t2) ->
       match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
-  | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
+  | GCast(c1, CastCoerce), NCast(c2, CastCoerce) ->
       match_in u alp metas sigma c1 c2
-  | GSort (_,GType _), NSort (GType _) when not u -> sigma
-  | GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
+  | GSort (GType _), NSort (GType _) when not u -> sigma
+  | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma
 
@@ -1105,11 +1110,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
      otherwise how to ensure it corresponds to a well-typed eta-expansion;
      we make an exception for types which are metavariables: this is useful e.g.
      to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
-  | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+  | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
       let avoid =
-        free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in
+        free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
       let id' = Namegen.next_ident_away id avoid in
-      let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+      let t1 = Loc.tag @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_term_env alp sigma id2 t1
@@ -1119,7 +1124,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
           bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
-      match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
+      match_in u alp metas sigma (mkGApp Loc.ghost a1 (Loc.tag @@ GVar id')) b2
 
   | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
@@ -1132,7 +1137,7 @@ and match_binders u alp metas na1 na2 sigma b1 b2 =
   let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
   match_in u alp metas sigma b1 b2
 
-and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
+and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
   let (alp,sigma) =
@@ -1140,9 +1145,9 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let term_of_binder = function
-  | Name id -> GVar (Loc.ghost,id)
-  | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+let term_of_binder bi = Loc.tag @@ match bi with
+  | Name id -> GVar id
+  | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
 type glob_decl2 =
     (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
@@ -1157,7 +1162,7 @@ let match_notation_constr u c (metas,pat) =
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
-      GVar (Loc.ghost,x) in
+      Loc.tag @@GVar x in
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
     match typ with
     | NtnTypeConstr ->