[location] Use Loc.located for constr_expr.

This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.

Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.

6 files changed, 207 insertions, 227 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3ba5d985f..4f23dd2ab 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -97,79 +97,79 @@ let eq_universes u1 u2 =
   | Some l, Some l' -> l = l'
   | _, _ -> false
 
-let rec constr_expr_eq e1 e2 =
+let rec constr_expr_eq (_loc1, e1) (_loc2, e2) =
   if e1 == e2 then true
   else match e1, e2 with
   | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
-  | CFix(_,id1,fl1), CFix(_,id2,fl2) ->
+  | CFix(id1,fl1), CFix(id2,fl2) ->
       eq_located Id.equal id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
-  | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) ->
+  | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
       eq_located Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
-  | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+  | CProdN(bl1,a1), CProdN(bl2,a2) ->
       List.equal binder_expr_eq bl1 bl2 &&
       constr_expr_eq a1 a2
-  | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+  | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
       List.equal binder_expr_eq bl1 bl2 &&
       constr_expr_eq a1 a2
-  | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) ->
+  | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
       Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
-  | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) ->
+  | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
       Option.equal Int.equal proj1 proj2 &&
       eq_reference r1 r2 &&
       List.equal constr_expr_eq al1 al2
-  | CApp(_,(proj1,e1),al1), CApp(_,(proj2,e2),al2) ->
+  | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
       Option.equal Int.equal proj1 proj2 &&
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
-  | CRecord (_, l1), CRecord (_, l2) ->
+  | CRecord l1, CRecord l2 ->
     let field_eq (r1, e1) (r2, e2) =
       eq_reference r1 r2 && constr_expr_eq e1 e2
     in
     List.equal field_eq l1 l2
-  | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
+  | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
       (** Don't care about the case_style *)
       Option.equal constr_expr_eq r1 r2 &&
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
-  | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) ->
+  | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
     List.equal (eq_located Name.equal) n1 n2 &&
     Option.equal (eq_located Name.equal) m1 m2 &&
     Option.equal constr_expr_eq e1 e2 &&
     constr_expr_eq t1 t2 &&
     constr_expr_eq b1 b2
-  | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) ->
+  | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
     constr_expr_eq e1 e2 &&
     Option.equal (eq_located Name.equal) n1 n2 &&
     Option.equal constr_expr_eq r1 r2 &&
     constr_expr_eq t1 t2 &&
     constr_expr_eq f1 f2
   | CHole _, CHole _ -> true
-  | CPatVar(_,i1), CPatVar(_,i2) ->
+  | CPatVar i1, CPatVar i2 ->
     Id.equal i1 i2
-  | CEvar (_, id1, c1), CEvar (_, id2, c2) ->
+  | CEvar (id1, c1), CEvar (id2, c2) ->
     Id.equal id1 id2 && List.equal instance_eq c1 c2
-  | CSort(_,s1), CSort(_,s2) ->
+  | CSort s1, CSort s2 ->
     Miscops.glob_sort_eq s1 s2
-  | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
+  | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) ->
       constr_expr_eq a1 a2 &&
       constr_expr_eq b1 b2
-  | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
+  | CCast(a1,CastCoerce), CCast(a2, CastCoerce) ->
       constr_expr_eq a1 a2
-  | CNotation(_, n1, s1), CNotation(_, n2, s2) ->
+  | CNotation(n1, s1), CNotation(n2, s2) ->
       String.equal n1 n2 &&
       constr_notation_substitution_eq s1 s2
-  | CPrim(_,i1), CPrim(_,i2) ->
+  | CPrim i1, CPrim i2 ->
     prim_token_eq i1 i2
-  | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
+  | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) ->
     binding_kind_eq bk1 bk2 &&
     Option.equal abstraction_kind_eq ak1 ak2 &&
     constr_expr_eq e1 e2
-  | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
+  | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
     String.equal s1 s2 &&
     constr_expr_eq e1 e2
   | _ -> false
@@ -228,29 +228,7 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
 and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && constr_expr_eq c1 c2
 
-let constr_loc = function
-  | CRef (Ident (loc,_),_) -> loc
-  | CRef (Qualid (loc,_),_) -> loc
-  | CFix (loc,_,_) -> loc
-  | CCoFix (loc,_,_) -> loc
-  | CProdN (loc,_,_) -> loc
-  | CLambdaN (loc,_,_) -> loc
-  | CLetIn (loc,_,_,_,_) -> loc
-  | CAppExpl (loc,_,_) -> loc
-  | CApp (loc,_,_) -> loc
-  | CRecord (loc,_) -> loc
-  | CCases (loc,_,_,_,_) -> loc
-  | CLetTuple (loc,_,_,_,_) -> loc
-  | CIf (loc,_,_,_,_) -> loc
-  | CHole (loc,_,_,_) -> loc
-  | CPatVar (loc,_) -> loc
-  | CEvar (loc,_,_) -> loc
-  | CSort (loc,_) -> loc
-  | CCast (loc,_,_) -> loc
-  | CNotation (loc,_,_) -> loc
-  | CGeneralization (loc,_,_,_) -> loc
-  | CPrim (loc,_) -> loc
-  | CDelimiters (loc,_,_) -> loc
+let constr_loc (l,_) = l
 
 let cases_pattern_expr_loc (l,_) = l
 
@@ -270,18 +248,18 @@ let local_binders_loc bll = match bll with
 
 (** Pseudo-constructors *)
 
-let mkIdentC id  = CRef (Ident (Loc.ghost, id),None)
-let mkRefC r     = CRef (r,None)
-let mkCastC (a,k)  = CCast (Loc.ghost,a,k)
-let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
-let mkLetInC (id,a,t,b)   = CLetIn (Loc.ghost,id,a,t,b)
-let mkProdC (idl,bk,a,b)   = CProdN (Loc.ghost,[idl,bk,a],b)
+let mkIdentC id   = Loc.tag @@ CRef (Ident (Loc.ghost, id),None)
+let mkRefC r      = Loc.tag @@ CRef (r,None)
+let mkCastC (a,k) = Loc.tag @@ CCast (a,k)
+let mkLambdaC (idl,bk,a,b) = Loc.tag @@ CLambdaN ([idl,bk,a],b)
+let mkLetInC  (id,a,t,b)   = Loc.tag @@ CLetIn (id,a,t,b)
+let mkProdC   (idl,bk,a,b) = Loc.tag @@ CProdN ([idl,bk,a],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
   match f with
-  | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
-  | _ -> CApp (Loc.ghost, (None, f), l)
+  | _loc, CApp (g,l') -> Loc.tag @@ CApp (g, l' @ l)
+  | _                 -> Loc.tag @@ CApp ((None, f), l)
 
 let add_name_in_env env n =
   match snd n with
@@ -290,47 +268,47 @@ let add_name_in_env env n =
 
 let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
 
-let expand_binders mkC loc bl c =
-  let rec loop loc bl c =
+let expand_binders ~loc mkC bl c =
+  let rec loop ~loc bl c =
     match bl with
     | [] -> ([], c)
     | b :: bl ->
         match b with
         | CLocalDef ((loc1,_) as n, oty, b) ->
-            let env, c = loop (Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
             let env = add_name_in_env env n in
-            (env, CLetIn (loc,n,oty,b,c))
+            (env, Loc.tag ~loc @@ CLetIn (n,oty,b,c))
         | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
-            let env, c = loop (Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
             let env = List.fold_left add_name_in_env env nl in
-            (env, mkC loc (nl,bk,t) c)
+            (env, mkC ~loc (nl,bk,t) c)
         | CLocalAssum ([],_,_) -> loop loc bl c
         | CLocalPattern (loc1, p, ty) ->
-            let env, c = loop (Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
             let ni = Hook.get fresh_var env c in
             let id = (loc1, Name ni) in
             let ty = match ty with
                  | Some ty -> ty
-                 | None -> CHole (loc1, None, IntroAnonymous, None)
+                 | None -> Loc.tag ~loc:loc1 @@ CHole (None, IntroAnonymous, None)
             in
-            let e = CRef (Libnames.Ident (loc1, ni), None) in
-            let c =
+            let e = Loc.tag @@ CRef (Libnames.Ident (loc1, ni), None) in
+            let c = Loc.tag ~loc @@
               CCases
-                (loc, LetPatternStyle, None, [(e,None,None)],
-                 [(loc1, ([(loc1,[p])], c))])
+                (LetPatternStyle, None, [(e,None,None)],
+                 [(Loc.tag ~loc:loc1 ([(loc1,[p])], c))])
             in
-            (ni :: env, mkC loc ([id],Default Explicit,ty) c)
+            (ni :: env, mkC ~loc ([id],Default Explicit,ty) c)
   in
   let (_, c) = loop loc bl c in
   c
 
-let mkCProdN loc bll c =
-  let mk loc b c = CProdN (loc,[b],c) in
-  expand_binders mk loc bll c
+let mkCProdN ~loc bll c =
+  let mk ~loc b c = Loc.tag ~loc @@ CProdN ([b],c) in
+  expand_binders ~loc mk bll c
 
-let mkCLambdaN loc bll c =
-  let mk loc b c = CLambdaN (loc,[b],c) in
-  expand_binders mk loc bll c
+let mkCLambdaN ~loc bll c =
+  let mk ~loc b c = Loc.tag ~loc @@ CLambdaN ([b],c) in
+  expand_binders ~loc mk bll c
 
 (* Deprecated *)
 let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
@@ -343,14 +321,14 @@ let coerce_reference_to_id = function
         (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | CRef (Ident (loc,id),_) -> (loc,id)
+  | _loc, CRef (Ident (loc,id),_) -> (loc,id)
   | a -> CErrors.user_err ~loc:(constr_loc a)
        ~hdr:"coerce_to_id"
          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | CRef (Ident (loc,id),_) -> (loc,Name id)
-  | CHole (loc,_,_,_) -> (loc,Anonymous)
+  | _loc, CRef (Ident (loc,id),_) -> (loc,Name id)
+  | loc, CHole (_,_,_) -> (loc,Anonymous)
   | a -> CErrors.user_err
          ~loc:(constr_loc a) ~hdr:"coerce_to_name"
          (str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index f6d97e107..ae5ec2be5 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -49,10 +49,10 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
 val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCLambdaN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
 
-val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCProdN : loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
 (** @deprecated variant of mkCLambdaN *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7a229856e..255de8500 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -144,7 +144,7 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
 
 let insert_delimiters e = function
   | None -> e
-  | Some sc -> CDelimiters (Loc.ghost,sc,e)
+  | Some sc -> Loc.tag @@ CDelimiters (sc,e)
 
 let insert_pat_delimiters loc p = function
   | None -> p
@@ -157,7 +157,7 @@ let insert_pat_alias loc p = function
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let extern_evar loc n l = CEvar (loc,n,l)
+let extern_evar loc n l = Loc.tag @@ CEvar (n,l)
 
 (** We allow customization of the global_reference printer.
     For instance, in the debugger the tables of global references
@@ -236,7 +236,7 @@ let expand_curly_brackets loc mknot ntn l =
   (* side effect *)
   mknot (loc,!ntn',l)
 
-let destPrim = function CPrim(_,t) -> Some t | _ -> None
+let destPrim = function _loc, CPrim t -> Some t | _ -> None
 let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
@@ -259,11 +259,11 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
 
 let make_notation loc ntn (terms,termlists,binders as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binders) then
-    CNotation (loc,ntn,subst)
+    Loc.tag ~loc @@ CNotation (ntn,subst)
   else
     make_notation_gen loc ntn
-      (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
-      (fun (loc,p) -> CPrim (loc,p))
+      (fun (loc,ntn,l) -> Loc.tag ~loc @@ CNotation (ntn,(l,[],[])))
+      (fun (loc,p) -> Loc.tag ~loc @@ CPrim p)
       destPrim terms
 
 let make_pat_notation loc ntn (terms,termlists as subst) args =
@@ -462,11 +462,11 @@ let is_projection nargs = function
 	 else None
      with Not_found -> None)
   | _ -> None
-	
+
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
 let is_significant_implicit a =
-  not (is_hole a)
+  not (is_hole (snd a))
 
 let is_needed_for_correct_partial_application tail imp =
   List.is_empty tail && not (maximal_insertion_of imp)
@@ -512,16 +512,16 @@ 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
-	  CApp (loc,(ip,f),args1@args2)
+	  Loc.tag ~loc @@ CApp ((ip,f),args1@args2)
     | None ->
       let args = exprec 1 (args,impl) in
-	if List.is_empty args then f else CApp (loc, (None, f), args)
+	if List.is_empty args then f else Loc.tag ~loc @@ CApp ((None, f), args)
   in
     try expl ()
     with Expl -> 
-      let f',us = match f with 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
-	CAppExpl (loc, (ip, f', us), List.map Lazy.force args)
+	Loc.tag ~loc @@ CAppExpl ((ip, f', us), List.map Lazy.force args)
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -530,23 +530,23 @@ let is_start_implicit = function
 let extern_global loc impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
-    CAppExpl (loc, (None, f, us), [])
+    Loc.tag ~loc @@ CAppExpl ((None, f, us), [])
   else
-    CRef (f,us)
+    Loc.tag ~loc @@ CRef (f,us)
 
 let extern_app loc inctx impl (cf,f) us args =
   if List.is_empty args then
     (* If coming from a notation "Notation a := @b" *)
-    CAppExpl (loc, (None, f, us), [])
+    Loc.tag ~loc @@ 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
-    CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
+    Loc.tag ~loc @@ CAppExpl ((is_projection (List.length args) cf,f,us), args)
   else
-    explicitize loc inctx impl (cf,CRef (f,us)) args
+    explicitize loc inctx impl (cf, Loc.tag ~loc @@ CRef (f,us)) args
 
 let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
 | [], _ -> []
@@ -600,7 +600,7 @@ let extern_possible_prim_token scopes r =
     let (sc,n) = uninterp_prim_token r in
     match availability_of_prim_token n sc scopes with
     | None -> None
-    | Some key -> Some (insert_delimiters (CPrim (loc_of_glob_constr r,n)) key)
+    | Some key -> Some (insert_delimiters (Loc.tag ~loc:(loc_of_glob_constr r) @@ CPrim n) key)
   with No_match ->
     None
 
@@ -608,7 +608,7 @@ let extern_optimal_prim_token scopes r r' =
   let c = extern_possible_prim_token scopes r in
   let c' = if r==r' then None else extern_possible_prim_token scopes r' in
   match c,c' with
-  | Some n, (Some (CDelimiters _) | None) | _, Some n -> n
+  | Some n, (Some ((_, CDelimiters _)) | None) | _, Some n -> n
   | _ -> raise No_match
 
 (**********************************************************************)
@@ -647,16 +647,16 @@ let rec extern inctx scopes vars r =
       extern_global loc (select_stronger_impargs (implicits_of_global ref))
         (extern_reference loc vars ref) (extern_universes us)
 
-  | GVar (loc,id) -> CRef (Ident (loc,id),None)
+  | GVar (loc,id) -> Loc.tag ~loc @@ CRef (Ident (loc,id),None)
 
-  | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, Misctypes.IntroAnonymous, None)
+  | GEvar (loc,n,[]) when !print_meta_as_hole -> Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)
 
   | GEvar (loc,n,l) ->
       extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,(b,n)) ->
-      if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
-        if b then CPatVar (loc,n) else CEvar (loc,n,[])
+  | GPatVar (loc,(b,n)) -> Loc.tag ~loc @@
+      if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
+        if b then CPatVar n else CEvar (n,[])
 
   | GApp (loc,f,args) ->
       (match f with
@@ -701,7 +701,7 @@ 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
-		 CRecord (loc, List.rev (ip projs locals args []))
+		 Loc.tag ~loc @@ CRecord (List.rev (ip projs locals args []))
 	       with
 		 | Not_found | No_match | Exit ->
                     let args = extern_args (extern true) vars args in
@@ -715,19 +715,19 @@ let rec extern inctx scopes vars r =
              (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
 
   | GLetIn (loc,na,b,t,c) ->
-      CLetIn (loc,(loc,na),sub_extern false scopes vars b,
+      Loc.tag ~loc @@ 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) ->
       let t = extern_typ scopes vars t in
       let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
-      CProdN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
+      Loc.tag ~loc @@ CProdN ([(Loc.ghost,na)::idl,Default bk,t],c)
 
   | GLambda (loc,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
-      CLambdaN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
+      Loc.tag ~loc @@ CLambdaN ([(Loc.ghost,na)::idl,Default bk,t],c)
 
   | GCases (loc,sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -757,17 +757,17 @@ let rec extern inctx scopes vars r =
                 tml
     in
     let eqns = List.map (extern_eqn inctx scopes vars) eqns in
-    CCases (loc,sty,rtntypopt',tml,eqns)
+    Loc.tag ~loc @@ CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (loc,nal,(na,typopt),tm,b) ->
-      CLetTuple (loc,List.map (fun na -> (Loc.ghost,na)) nal,
+      Loc.tag ~loc @@ 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) ->
-      CIf (loc,sub_extern false scopes vars c,
+      Loc.tag ~loc @@ 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)
@@ -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
-	     CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
+	     Loc.tag ~loc @@ CFix ((loc,idv.(n)),Array.to_list listdecl)
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
@@ -803,14 +803,14 @@ 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
-	     CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
+	     Loc.tag ~loc @@ CCoFix ((loc,idv.(n)),Array.to_list listdecl))
 
-  | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
+  | GSort (loc,s) -> Loc.tag ~loc @@ CSort (extern_glob_sort s)
 
-  | GHole (loc,e,naming,_) -> CHole (loc, Some e, naming, None) (** TODO: extern tactics. *)
+  | GHole (loc,e,naming,_) -> Loc.tag ~loc @@ CHole (Some e, naming, None) (** TODO: extern tactics. *)
 
   | GCast (loc,c, c') ->
-      CCast (loc,sub_extern true scopes vars c,
+      Loc.tag ~loc @@ CCast (sub_extern true scopes vars c,
 	     Miscops.map_cast_type (extern_typ scopes vars) c')
 
 and extern_typ (_,scopes) =
@@ -821,7 +821,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 and factorize_prod scopes vars na bk aty c =
   let c = extern_typ scopes vars c in
   match na, c with
-  | Name id, CProdN (loc,[nal,Default bk',ty],c)
+  | Name id, (loc, CProdN ([nal,Default bk',ty],c))
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
@@ -831,7 +831,7 @@ and factorize_prod scopes vars na bk aty c =
 and factorize_lambda inctx scopes vars na bk aty c =
   let c = sub_extern inctx scopes vars c in
   match c with
-  | CLambdaN (loc,[nal,Default bk',ty],c)
+  | loc, CLambdaN ([nal,Default bk',ty],c)
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
@@ -940,7 +940,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
 		  extern true (scopt,scl@scopes) vars c, None)
 		  terms in
               let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
-	      if List.is_empty l then a else CApp (loc,(None,a),l) in
+	      Loc.tag ~loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in
  	if List.is_empty args then e
 	else
 	  let args = fill_arg_scopes args argsscopes scopes in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6bf6772c6..4af89e1ef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -217,7 +217,7 @@ let contract_notation ntn (l,ll,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CNotation (_,"{ _ }",([a],[],[])) :: l ->
+    | (_loc, CNotation ("{ _ }",([a],[],[]))) :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	  let name =
 	    let id =
 	      match ty with
-	      | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
+	      | _, CApp ((_, (_, CRef (Ident (loc,id),_))), _) -> id
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -448,7 +448,7 @@ let intern_local_pattern intern lvar env p =
   List.fold_left
     (fun env (loc, i) ->
        let bk = Default Implicit in
-       let ty = CHole (loc, None, Misctypes.IntroAnonymous, None) in
+       let ty = Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
        let n = Name i in
        let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
        env)
@@ -479,7 +479,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+        | None -> Loc.tag ~loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
       let il = List.map snd (free_vars_of_pat [] p) in
@@ -592,15 +592,15 @@ let rec subordinate_letins letins = function
 
 let terms_of_binders bl =
   let rec term_of_pat = function
-    | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
+    | PatVar (loc,Name id)   -> Loc.tag ~loc @@ CRef (Ident (loc,id), None)
     | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (loc,c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+       let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
-       CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+       Loc.tag ~loc @@ CAppExpl ((None,r,None),params @ List.map term_of_pat l) in
   let rec extract_variables = function
-    | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l
+    | GLocalAssum (loc,Name id,_,_)::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
     | GLocalDef (loc,Anonymous,_,_,_)::l
     | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
@@ -754,7 +754,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
-      (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> Loc.tag ~loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -1515,15 +1515,15 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
-  let rec intern env = function
-    | CRef (ref,us) as x ->
+  let rec intern env = Loc.with_loc (fun ~loc -> function
+    | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
-	  intern_applied_reference intern env (Environ.named_context globalenv) 
-	    lvar us [] ref 
+	  intern_applied_reference intern env (Environ.named_context globalenv)
+	    lvar us [] ref
 	in
-	  apply_impargs c env imp subscopes l (constr_loc x)
+	  apply_impargs c env imp subscopes l loc
 
-    | CFix (loc, (locid,iddef), dl) ->
+    | CFix ((locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
@@ -1564,7 +1564,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
               Array.map (fun (_,bl,_,_) -> bl) idl,
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
-    | CCoFix (loc, (locid,iddef), dl) ->
+    | CCoFix ((locid,iddef), dl) ->
         let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
@@ -1589,33 +1589,33 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
               Array.map (fun (bl,_,_) -> bl) idl,
               Array.map (fun (_,ty,_) -> ty) idl,
               Array.map (fun (_,_,bd) -> bd) idl)
-    | CProdN (loc,[],c2) ->
+    | CProdN ([],c2) ->
         intern_type env c2
-    | CProdN (loc,(nal,bk,ty)::bll,c2) ->
-        iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
-    | CLambdaN (loc,[],c2) ->
+    | CProdN ((nal,bk,ty)::bll,c2) ->
+        iterate_prod loc env bk ty (Loc.tag ~loc @@ CProdN (bll, c2)) nal
+    | CLambdaN ([],c2) ->
         intern env c2
-    | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
-    | CLetIn (loc,na,c1,t,c2) ->
+    | CLambdaN ((nal,bk,ty)::bll,c2) ->
+	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ~loc @@ CLambdaN (bll, c2)) nal
+    | 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,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
+    | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
 	when Bigint.is_strictly_pos p ->
-	intern env (CPrim (loc,Numeral (Bigint.neg p)))
-    | CNotation (_,"( _ )",([a],[],[])) -> intern env a
-    | CNotation (loc,ntn,args) ->
+	intern env (Loc.tag ~loc @@ CPrim (Numeral (Bigint.neg p)))
+    | CNotation ("( _ )",([a],[],[])) -> intern env a
+    | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
-    | CGeneralization (loc,b,a,c) ->
+    | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
-    | CPrim (loc, p) ->
+    | CPrim p ->
 	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
-    | CDelimiters (loc, key, e) ->
+    | CDelimiters (key, e) ->
 	intern {env with tmp_scope = None;
 		  scopes = find_delimiters_scope loc key :: env.scopes} e
-    | CAppExpl (loc, (isproj,ref,us), args) ->
+    | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
@@ -1624,42 +1624,42 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  (* Rem: GApp(_,f,[]) stands for @f *)
 	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
 
-    | CApp (loc, (isproj,f), args) ->
+    | CApp ((isproj,f), args) ->
         let f,args = match f with
           (* Compact notations like "t.(f args') args" *)
-          | CApp (_,(Some _,f), args') when not (Option.has_some isproj) -> 
+          | _loc, CApp ((Some _,f), args') when not (Option.has_some isproj) ->
 	    f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> f,args in
 	let (c,impargs,args_scopes,l),args =
           match f with
-            | CRef (ref,us) -> 
+            | _loc, CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
-            | CNotation (loc,ntn,([],[],[])) ->
+            | _loc, CNotation (ntn,([],[],[])) ->
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
             | x -> (intern env f,[],[],[]), args in
-          apply_impargs c env impargs args_scopes 
+          apply_impargs c env impargs args_scopes
 	    (merge_impargs l args) loc
 
-    | CRecord (loc, fs) ->
+    | CRecord fs ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
-                                                 Misctypes.IntroAnonymous, None))
+	             (fun _idx -> Loc.tag ~loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+                                                         Misctypes.IntroAnonymous, None))
        in
        begin
 	  match fields with
 	    | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
-                let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
+		let pars = List.make n (Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let app = Loc.tag ~loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
-    | CCases (loc, sty, rtnpo, tms, eqns) ->
+    | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
             (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
@@ -1701,7 +1701,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
-    | CLetTuple (loc, nal, (na,po), b, c) ->
+    | CLetTuple (nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
@@ -1711,7 +1711,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  intern_type env'' u) po in
         GLetTuple (loc, 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 (loc, c, (na,po), b1, b2) ->
+    | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
@@ -1719,7 +1719,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    (Loc.ghost,na') in
 	  intern_type env'' p) po in
         GIf (loc, c', (na', p'), intern env b1, intern env b2)
-    | CHole (loc, k, naming, solve) ->
+    | CHole (k, naming, solve) ->
         let k = match k with
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -1745,22 +1745,22 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         in
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar (loc, n) when allow_patvar ->
+    | CPatVar n when allow_patvar ->
 	GPatVar (loc, (true,n))
-    | CEvar (loc, n, []) when allow_patvar ->
+    | CEvar (n, []) when allow_patvar ->
 	GPatVar (loc, (false,n))
     (* end *)
     (* Parsing existential variables *)
-    | CEvar (loc, n, l) ->
+    | CEvar (n, l) ->
 	GEvar (loc, n, List.map (on_snd (intern env)) l)
-    | CPatVar (loc, _) ->
+    | CPatVar _ ->
         raise (InternalizationError (loc,IllegalMetavariable))
     (* end *)
-    | CSort (loc, s) ->
+    | CSort s ->
 	GSort(loc,s)
-    | CCast (loc, c1, c2) ->
+    | CCast (c1, c2) ->
         GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
-
+  )
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind =
@@ -1887,17 +1887,17 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  intern_args env subscopes rargs
     in aux 1 l subscopes eargs rargs
 
-  and apply_impargs c env imp subscopes l loc = 
+  and apply_impargs c env imp subscopes l loc =
     let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
     let l = intern_impargs c env imp subscopes l in
       smart_gapp c loc l
 
   and smart_gapp f loc = function
     | [] -> f
-    | l -> match f with 
+    | 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)
-      
+
   and intern_args env subscopes = function
     | [] -> []
     | a::args ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7f11c0a3b..d2bebfb54 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,11 +92,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
       else ungeneralizable loc id
     else l
   in
-  let rec aux bdvars l c = match c with
+  let rec aux bdvars l (loc, c) = match c with
     | CRef (Ident (loc,id),_) -> found loc id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) ->
-	Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
-    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
+    | CNotation ("{ _ : _ | _ }", ((_, CRef (Ident (_, id),_)) :: _, [], [])) when not (Id.Set.mem id bdvars) ->
+	Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l (loc, c)
+    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l (loc, c)
   in aux bound l c
 
 let ids_of_names l =
@@ -251,18 +251,18 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, decl) ->
     let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
+      (Loc.tag @@ CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
 
-let destClassApp cl =
+let destClassApp (loc, cl) =
   match cl with
-    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
-    | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
+    | CApp ((None, (_loc, CRef (ref, inst))), l) -> loc, ref, List.map fst l, inst
+    | CAppExpl ((None, ref, inst), l) -> loc, ref, l, inst
     | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
-let destClassAppExpl cl =
+let destClassAppExpl (loc, cl) =
   match cl with
-    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
+    | CApp ((None, (_loc, CRef (ref, inst))), l) -> loc, ref, l, inst
     | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
@@ -295,7 +295,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    CAppExpl (loc, (None, id, inst), args), avoid
+	    Loc.tag ~loc @@ CAppExpl ((None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 172caa2ca..c3e341d74 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -103,49 +103,50 @@ let rec fold_local_binders g f n acc b = function
   | [] ->
       f n acc b
 
-let fold_constr_expr_with_binders g f n acc = function
-  | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l
-  | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
-  | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l
-  | CLetIn (_,na,a,t,b) ->
+let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ~loc -> function
+  | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
+  | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+  | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
+  | CLetIn (na,a,t,b) ->
      f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
-  | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
-  | CCast (loc,a,CastCoerce) -> f n acc a
-  | CNotation (_,_,(l,ll,bll)) ->
+  | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
+  | CCast (a,CastCoerce) -> f n acc a
+  | CNotation (_,(l,ll,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
-      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,IntroAnonymous,None)) bl) acc bll
-  | CGeneralization (_,_,_,c) -> f n acc c
-  | CDelimiters (loc,_,a) -> f n acc a
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (Loc.tag @@ CHole (None,IntroAnonymous,None)) bl) acc bll
+  | CGeneralization (_,_,c) -> f n acc c
+  | CDelimiters (_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
       acc
-  | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
-  | CCases (loc,sty,rtnpo,al,bl) ->
+  | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+  | CCases (sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
       List.fold_right (fun (loc,(patl,rhs)) acc ->
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
-  | CLetTuple (loc,nal,(ona,po),b,c) ->
+  | CLetTuple (nal,(ona,po),b,c) ->
       let n' = List.fold_right (Loc.down_located (name_fold g)) nal n in
       f (Option.fold_right (Loc.down_located (name_fold g)) ona n') (f n acc b) c
-  | CIf (_,c,(ona,po),b1,b2) ->
+  | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
 	(f (Option.fold_right (Loc.down_located (name_fold g)) ona n)) acc po
-  | CFix (loc,_,l) ->
+  | CFix (_,l) ->
       let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
 	fold_local_binders g f n'
 	  (fold_local_binders g f n acc t lb) c lb) l acc
-  | CCoFix (loc,_,_) ->
+  | CCoFix (_,_) ->
       Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+  )
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-  | CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l
+  | _loc, CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l
   | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
   in aux [] Id.Set.empty c
 
@@ -209,60 +210,61 @@ let map_local_binders f g e bl =
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
-let map_constr_expr_with_binders g f e = function
-  | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
-  | CApp (loc,(p,a),l) ->
-      CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
-  | CProdN (loc,bl,b) ->
-      let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
-  | CLambdaN (loc,bl,b) ->
-      let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
-  | CLetIn (loc,na,a,t,b) ->
-      CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
-  | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c)
-  | CNotation (loc,n,(l,ll,bll)) ->
+let map_constr_expr_with_binders g f e = Loc.map (function
+  | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
+  | CApp ((p,a),l) ->
+      CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
+  | CProdN (bl,b) ->
+      let (e,bl) = map_binders f g e bl in CProdN (bl,f e b)
+  | CLambdaN (bl,b) ->
+      let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
+  | CLetIn (na,a,t,b) ->
+      CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+  | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
+  | CNotation (n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
-      CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll,
+      CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll,
                      List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
-  | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
-  | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
+  | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
+  | CDelimiters (s,a) -> CDelimiters (s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _
   | CPrim _ | CRef _ as x -> x
-  | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
-  | CCases (loc,sty,rtnpo,a,bl) ->
+  | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
+  | CCases (sty,rtnpo,a,bl) ->
       let bl = List.map (fun (loc,(patl,rhs)) ->
         let ids = ids_of_pattern_list patl in
         (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
-      CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
-  | CLetTuple (loc,nal,(ona,po),b,c) ->
+      CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
+  | CLetTuple (nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
       let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
-      CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
-  | CIf (loc,c,(ona,po),b1,b2) ->
+      CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
+  | CIf (c,(ona,po),b1,b2) ->
       let e' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
-      CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
-  | CFix (loc,id,dl) ->
-      CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
+      CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
+  | CFix (id,dl) ->
+      CFix (id,List.map (fun (id,n,bl,t,d) ->
         let (e',bl') = map_local_binders f g e bl in
         let t' = f e' t in
         (* Note: fix names should be inserted before the arguments... *)
         let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
         let d' = f e'' d in
         (id,n,bl',t',d')) dl)
-  | CCoFix (loc,id,dl) ->
-      CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+  | CCoFix (id,dl) ->
+      CCoFix (id,List.map (fun (id,bl,t,d) ->
         let (e',bl') = map_local_binders f g e bl in
         let t' = f e' t in
         let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
         let d' = f e'' d in
         (id,bl',t',d')) dl)
+  )
 
 (* Used in constrintern *)
 let rec replace_vars_constr_expr l = function
-  | CRef (Ident (loc,id),us) as x ->
-      (try CRef (Ident (loc,Id.Map.find id l),us) with Not_found -> x)
+  | loc, CRef (Ident (loc_id,id),us) as x ->
+      (try loc, CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x)
   | c -> map_constr_expr_with_binders Id.Map.remove
            replace_vars_constr_expr l c