[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

12 files changed, 217 insertions, 213 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 61115c00b5..4b61ab4946 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -242,13 +242,12 @@ let local_binder_loc = function
   | CLocalPattern (loc,_) -> loc
 
 let local_binders_loc bll = match bll with
-  | [] -> Loc.ghost
-  | h :: l ->
-    Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll))
+  | []     -> None
+  | h :: l -> Some (Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll)))
 
 (** Pseudo-constructors *)
 
-let mkIdentC id   = Loc.tag @@ CRef (Ident (Loc.ghost, id),None)
+let mkIdentC id   = Loc.tag @@ CRef (Ident (Loc.tag 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)
@@ -268,23 +267,23 @@ let add_name_in_env env n =
 
 let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
 
-let expand_binders ~loc mkC 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:(Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.opt_merge loc1 loc) bl c in
             let env = add_name_in_env env n in
-            (env, Loc.tag ~loc @@ CLetIn (n,oty,b,c))
+            (env, Loc.tag ?loc @@ CLetIn (n,oty,b,c))
         | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
-            let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.opt_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)
-        | CLocalAssum ([],_,_) -> loop loc bl c
+            (env, mkC ?loc (nl,bk,t) c)
+        | CLocalAssum ([],_,_) -> loop ?loc bl c
         | CLocalPattern (loc1, (p, ty)) ->
-            let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
+            let env, c = loop ~loc:(Loc.opt_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
@@ -292,27 +291,27 @@ let expand_binders ~loc mkC bl c =
                  | None -> Loc.tag ~loc:loc1 @@ CHole (None, IntroAnonymous, None)
             in
             let e = Loc.tag @@ CRef (Libnames.Ident (loc1, ni), None) in
-            let c = Loc.tag ~loc @@
+            let c = Loc.tag ?loc @@
               CCases
                 (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
+  let (_, c) = loop ?loc bl c in
   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 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 = Loc.tag ~loc @@ CLambdaN ([b],c) in
-  expand_binders ~loc mk 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
-let prod_constr_expr c bl =  mkCProdN (local_binders_loc bl) bl c
+let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
+let prod_constr_expr c bl =  mkCProdN ?loc:(local_binders_loc bl) bl c
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index ae5ec2be5c..82e4f54b08 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 val constr_loc : constr_expr -> Loc.t
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
 val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
-val local_binders_loc : local_binder_expr list -> Loc.t
+val local_binders_loc : local_binder_expr list -> Loc.t option
 
 (** {6 Constructors}*)
 
@@ -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: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: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 8d9f8552dc..5960a6baa5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -146,13 +146,13 @@ let insert_delimiters e = function
   | None -> e
   | Some sc -> Loc.tag @@ CDelimiters (sc,e)
 
-let insert_pat_delimiters loc p = function
+let insert_pat_delimiters ?loc p = function
   | None -> p
-  | Some sc -> Loc.tag ~loc @@ CPatDelimiters (sc,p)
+  | Some sc -> Loc.tag ?loc @@ CPatDelimiters (sc,p)
 
-let insert_pat_alias loc p = function
+let insert_pat_alias ?loc p = function
   | Anonymous -> p
-  | Name id -> Loc.tag ~loc @@ CPatAlias (p,id)
+  | Name id -> Loc.tag ?loc @@ CPatAlias (p,id)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -163,15 +163,15 @@ let extern_evar n l = CEvar (n,l)
     For instance, in the debugger the tables of global references
     may be inaccurate *)
 
-let default_extern_reference loc vars r =
-  Qualid (loc,shortest_qualid_of_global vars r)
+let default_extern_reference ?loc vars r =
+  Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
 let set_extern_reference f = my_extern_reference := f
 let get_extern_reference () = !my_extern_reference
 
-let extern_reference loc vars l = !my_extern_reference loc vars l
+let extern_reference ?loc vars l = !my_extern_reference ?loc vars l
 
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
@@ -266,16 +266,16 @@ let make_notation loc ntn (terms,termlists,binders as subst) =
       (fun (loc,p) -> Loc.tag ~loc @@ CPrim p)
       destPrim terms
 
-let make_pat_notation loc ntn (terms,termlists as subst) args =
-  if not (List.is_empty termlists) then (loc, CPatNotation (ntn,subst,args)) else
+let make_pat_notation ?loc ntn (terms,termlists as subst) args =
+  if not (List.is_empty termlists) then (Loc.tag ?loc @@ CPatNotation (ntn,subst,args)) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> Loc.tag ~loc @@ CPatNotation (ntn,(l,[]),args))
-    (fun (loc,p)     -> Loc.tag ~loc @@ CPatPrim p)
+    (fun (loc,ntn,l) -> Loc.tag ?loc @@ CPatNotation (ntn,(l,[]),args))
+    (fun (loc,p)     -> Loc.tag ?loc @@ CPatPrim p)
     destPatPrim terms
 
-let mkPat loc qid l =
+let mkPat ?loc qid l = Loc.tag ?loc @@
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
-  if List.is_empty l then Loc.tag ~loc @@ CPatAtom (Some qid) else Loc.tag ~loc @@ CPatCstr (qid,None,l)
+  if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -293,7 +293,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   match pat with
     | loc, PatCstr(cstrsp,args,na)
 	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
-      let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
+      let c = extern_reference ~loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
     | _ ->
@@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       | None -> raise No_match
       | Some key ->
 	let loc = cases_pattern_loc pat in
-	insert_pat_alias loc (insert_pat_delimiters loc (Loc.tag ~loc @@ CPatPrim p) key) na
+	insert_pat_alias ~loc (insert_pat_delimiters ~loc (Loc.tag ~loc @@ CPatPrim p) key) na
   with No_match ->
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -330,12 +330,12 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		      | (_loc, CPatAtom(None)) :: tail -> ip q tail acc
 		    (* we don't want to have 'x = _' in our patterns *)
 		      | head :: tail -> ip q tail
-		        ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+		        ((extern_reference ~loc Id.Set.empty (ConstRef c), head) :: acc)
 	      in
 	      Loc.tag ~loc @@ CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-                  let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
+                  let c = extern_reference ~loc Id.Set.empty (ConstructRef cstrsp) in
 		  if !Topconstr.asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then Loc.tag ~loc @@ CPatCstr (c, None, args)
@@ -345,8 +345,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
 		      | Some true_args -> Loc.tag ~loc @@ CPatCstr (c, None, true_args)
 		      | None           -> Loc.tag ~loc @@ CPatCstr (c, Some full_args, [])
-	  in insert_pat_alias loc p na
-and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
+	  in insert_pat_alias ~loc p na
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
   function
     | NotationRule (sc,ntn) ->
@@ -373,11 +373,11 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
 		  |Some true_args -> true_args
 		  |None -> raise No_match
 	    in
-	    insert_pat_delimiters loc
-	      (make_pat_notation loc ntn (l,ll) l2') key
+	    insert_pat_delimiters ?loc
+	      (make_pat_notation ?loc ntn (l,ll) l2') key
       end
     | SynDefRule kn ->
-      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+      let qid = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in
       let l1 =
 	List.rev_map (fun (c,(scopt,scl)) ->
           extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
@@ -390,7 +390,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
 	    |None -> raise No_match
       in
       assert (List.is_empty substlist);
-      mkPat loc qid (List.rev_append l1 l2')
+      mkPat ?loc qid (List.rev_append l1 l2')
 and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
@@ -398,9 +398,9 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = func
       if List.mem keyrule !print_non_active_notations then raise No_match;
       match t with
 	| PatCstr (cstr,_,na) ->
-	  let p = apply_notation_to_pattern loc (ConstructRef cstr)
+	  let p = apply_notation_to_pattern ~loc (ConstructRef cstr)
 	    (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in
-	  insert_pat_alias loc p na
+	  insert_pat_alias ~loc p na
 	| PatVar Anonymous -> Loc.tag ~loc @@ CPatAtom None
 	| PatVar (Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
     with
@@ -411,7 +411,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
   | (keyrule,pat,n as _rule)::rules ->
     try
       if List.mem keyrule !print_non_active_notations then raise No_match;
-      apply_notation_to_pattern Loc.ghost (IndRef ind)
+      apply_notation_to_pattern  (IndRef ind)
 	(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
     with
 	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
@@ -420,7 +420,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
-    let c = extern_reference Loc.ghost vars (IndRef ind) in
+    let c = extern_reference vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
     Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
@@ -430,14 +430,14 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
 	| Some key ->
-	  insert_pat_delimiters Loc.ghost (Loc.tag @@ CPatPrim p) key
+	  insert_pat_delimiters (Loc.tag @@ CPatPrim p) key
     with No_match ->
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
 	extern_notation_ind_pattern scopes vars ind args
 	  (uninterp_ind_pattern_notations ind)
     with No_match ->
-      let c = extern_reference Loc.ghost vars (IndRef ind) in
+      let c = extern_reference vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
 	   |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args)
@@ -490,7 +490,7 @@ let explicitize inctx impl (cf,f) args =
 	   is_significant_implicit (Lazy.force a))
 	in
         if visible then
-	  (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
+	  (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail
 	else
 	  tail
     | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
@@ -615,9 +615,11 @@ let extern_optimal_prim_token scopes r r' =
 (* mapping decl                                                       *)
 
 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,t) -> GLocalDef (loc,p,bk,x,Some t)
+  | (p,bk,None,t) -> GLocalAssum (p,bk,t)
+  | (p,bk,Some x,(_,GHole ( _, Misctypes.IntroAnonymous, None))) -> GLocalDef (p,bk,x,None)
+  | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t)
+
+let extended_glob_local_binder_of_decl ?loc u = Loc.tag ?loc (extended_glob_local_binder_of_decl loc u)
 
 (**********************************************************************)
 (* mapping glob_constr to constr_expr                                    *)
@@ -645,7 +647,7 @@ let rec extern inctx scopes vars r =
   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)
+        (extern_reference ~loc vars ref) (extern_universes us)
 
   | GVar id -> CRef (Ident (loc,id),None)
 
@@ -699,7 +701,7 @@ let rec extern inctx scopes vars r =
 				     (* we give up since the constructor is not complete *)
 				 | (arg, scopes) :: tail ->
                                      let head = extern true scopes vars arg in
-				     ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+				     ip q locs' tail ((extern_reference ~loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
 		 CRecord (List.rev (ip projs locals args []))
 	       with
@@ -707,7 +709,7 @@ let rec extern inctx scopes vars r =
                     let args = extern_args (extern true) vars args in
 		     extern_app inctx
 		       (select_stronger_impargs (implicits_of_global ref))
-		       (Some ref,extern_reference rloc vars ref) (extern_universes us) args
+		       (Some ref,extern_reference ~loc:rloc vars ref) (extern_universes us) args
 	     end
 
 	 | _       ->
@@ -722,12 +724,12 @@ let rec extern inctx scopes vars r =
   | 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
-      CProdN ([(Loc.ghost,na)::idl,Default bk,t],c)
+      CProdN ([(Loc.tag na)::idl,Default 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
-      CLambdaN ([(Loc.ghost,na)::idl,Default bk,t],c)
+      CLambdaN ([(Loc.tag na)::idl,Default bk,t],c)
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
@@ -741,12 +743,12 @@ let rec extern inctx scopes vars r =
                             | None -> None
                             | Some ntn ->
                                if occur_glob_constr id ntn then
-                                 Some (Loc.ghost, Anonymous)
+                                 Some (Loc.tag Anonymous)
                                else None
                       end
                    | Anonymous, _ -> None
                    | Name id, (_, GVar id') when Id.equal id id' -> None
-                   | Name _, _ -> Some (Loc.ghost,na) in
+                   | Name _, _ -> Some (Loc.tag na) in
                  (sub_extern false scopes vars tm,
                   na',
                   Option.map (fun (loc,(ind,nal)) ->
@@ -760,15 +762,15 @@ let rec extern inctx scopes vars r =
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
-      CLetTuple (List.map (fun na -> (Loc.ghost,na)) nal,
-        (Option.map (fun _ -> (Loc.ghost,na)) typopt,
+      CLetTuple (List.map (fun na -> (Loc.tag na)) nal,
+        (Option.map (fun _ -> (Loc.tag 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 (c,(na,typopt),b1,b2) ->
       CIf (sub_extern false scopes vars c,
-        (Option.map (fun _ -> (Loc.ghost,na)) typopt,
+        (Option.map (fun _ -> (Loc.tag na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
@@ -779,28 +781,28 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
-                 let bl = List.map (extended_glob_local_binder_of_decl loc) bl in
+                 let bl = List.map (extended_glob_local_binder_of_decl ~loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (Loc.ghost, out_name (List.nth assums x))
+		     | Some x -> Some (Loc.tag @@ out_name (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
-		 ((Loc.ghost, fi), (n, ro), bl, extern_typ scopes vars0 ty,
+		 ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in
 	     CFix ((loc,idv.(n)),Array.to_list listdecl)
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
-                 let bl = List.map (extended_glob_local_binder_of_decl loc) blv.(i) in
+                 let bl = List.map (extended_glob_local_binder_of_decl ~loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
                  let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
-		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
+		 ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
 	     CCoFix ((loc,idv.(n)),Array.to_list listdecl))
@@ -841,14 +843,14 @@ and factorize_lambda inctx scopes vars na bk aty c =
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
-  | GLocalDef (_,na,bk,bd,ty)::l ->
+  | (_, GLocalDef (na,bk,bd,ty))::l ->
       let (assums,ids,l) =
         extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
-       CLocalDef((Loc.ghost,na), extern false scopes vars bd,
+       CLocalDef((Loc.tag na), extern false scopes vars bd,
                    Option.map (extern false scopes vars) ty) :: l)
 
-  | GLocalAssum (_,na,bk,ty)::l ->
+  | (_, GLocalAssum (na,bk,ty))::l ->
       let ty = extern_typ scopes vars ty in
       (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
@@ -856,12 +858,12 @@ and extern_local_binder scopes vars = function
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
-               CLocalAssum((Loc.ghost,na)::nal,k,ty')::l)
+               CLocalAssum((Loc.tag na)::nal,k,ty')::l)
         | (assums,ids,l) ->
             (na::assums,na::ids,
-             CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l))
+             CLocalAssum([(Loc.tag na)],Default bk,ty) :: l))
 
-  | GLocalPattern (_,(p,_),_,bk,ty)::l ->
+  | (_, GLocalPattern ((p,_),_,bk,ty))::l ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
@@ -1078,5 +1080,5 @@ let extern_rel_context where env sigma sign =
   let where = Option.map EConstr.of_constr where in
   let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
-  let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
+  let a = List.map (extended_glob_local_binder_of_decl) a in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b39339450a..ea627cff11 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -37,7 +37,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -55,9 +55,9 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
 val get_extern_reference :
-  unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
 (** This governs printing of implicit arguments. If [with_implicits] is
    on and not [with_arguments] then implicit args are printed prefixed
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d1b931a227..585f038086 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -345,13 +345,13 @@ let rec check_capture ty = function
   | [] ->
       ()
 
-let locate_if_hole loc na = function
+let locate_if_hole ?loc na = function
   | _, GHole (_,naming,arg) ->
       (try match na with
-	| Name id -> glob_constr_of_notation_constr loc
+	| Name id -> glob_constr_of_notation_constr ?loc
 	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
-      with Not_found -> Loc.tag ~loc @@ GHole (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 =
@@ -424,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty =
       List.fold_left
 	(fun (env, bl) (loc, na as locna) ->
           (push_name_env lvar impls env locna,
-           (loc,(na,k,locate_if_hole loc na ty))::bl))
+           (loc,(na,k,locate_if_hole ~loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
@@ -454,27 +454,28 @@ let intern_local_pattern intern lvar env p =
        env)
     env (free_vars_of_pat [] p)
 
-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 glob_local_binder_of_extended = Loc.with_loc (fun ~loc -> function
+  | GLocalAssum (na,bk,t) -> (na,bk,None,t)
+  | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
+  | GLocalDef (na,bk,c,None) ->
       let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
       (na,bk,Some c,t)
-  | GLocalPattern (loc,_,_,_,_) ->
+  | GLocalPattern (_,_,_,_) ->
       Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
+  )
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
 let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern lvar env nal bk ty in
-      let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in
+      let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ~loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
   | CLocalDef((loc,na as locna),def,ty) ->
      let term = intern env def in
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
-       GLocalDef (loc,na,Explicit,term,ty) :: bl)
+       (Loc.tag ~loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
   | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
@@ -494,7 +495,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern lvar env [na] bk tyc in
       let _,(_,bk,t) = List.hd bl' in
-      (env, GLocalPattern(loc,(cp,il),id,bk,t) :: bl)
+      (env, (Loc.tag ~loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -582,13 +583,13 @@ let make_letins =
 let rec subordinate_letins letins = function
   (* binders come in reverse order; the non-let are returned in reverse order together *)
   (* with the subordinated let-in in writing order *)
-  | GLocalDef (loc,na,_,b,t)::l ->
+  | (loc, GLocalDef (na,_,b,t))::l ->
       subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
-  | GLocalAssum (loc,na,bk,t)::l ->
+  | (loc, GLocalAssum (na,bk,t))::l ->
       let letins',rest = subordinate_letins [] l in
       letins',((loc,(na,bk,t)),letins)::rest
-  | GLocalPattern (loc,u,id,bk,t) :: l ->
-      subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l)
+  | (loc, GLocalPattern (u,id,bk,t)) :: l ->
+      subordinate_letins (LPCases (loc,u,id)::letins) ([Loc.tag ~loc @@ GLocalAssum (Name id,bk,t)] @ l)
   | [] ->
       letins,[]
 
@@ -602,11 +603,11 @@ let terms_of_binders bl =
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | 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."
-    | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l
+    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
+    | (loc, GLocalDef (Anonymous,_,_,_))::l
+    | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
+    | (loc, GLocalPattern ((u,_),_,_,_)) :: l -> term_of_pat u :: extract_variables l
     | [] -> [] in
   extract_variables bl
 
@@ -697,7 +698,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos 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
+      glob_constr_of_notation_constr_with_binders ~loc
         (traverse_binder subst avoid) (aux subst') subinfos t
   and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
     (* subst remembers the delimiters stack in the interpretation *)
@@ -728,7 +729,7 @@ let make_subst ids l =
 
 let intern_notation intern env lvar loc ntn fullargs =
   let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
-  let ((ids,c),df) = interp_notation loc ntn (env.tmp_scope,env.scopes) in
+  let ((ids,c),df) = interp_notation ~loc ntn (env.tmp_scope,env.scopes) in
   Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
   let ids,idsl,idsbl = split_by_type ids in
   let terms = make_subst ids args in
@@ -809,8 +810,8 @@ let find_appl_head_data c =
 	List.skipn_at_least n scopes,[]
   | _ -> c,[],[],[]
 
-let error_not_enough_arguments loc =
-  user_err ~loc  (str "Abbreviation is not applied enough.")
+let error_not_enough_arguments ?loc =
+  user_err ?loc  (str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let is_unset (a, b) = match b with None -> false | Some _ -> true in
@@ -843,7 +844,7 @@ let intern_qualid loc qid intern env lvar us args =
   | SynDef sp ->
       let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
-      if List.length args < nids then error_not_enough_arguments loc;
+      if List.length args < nids then error_not_enough_arguments ~loc;
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
       let terms = make_subst ids (List.map fst args1) in
@@ -893,7 +894,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
 
 let interp_reference vars r =
   let (r,_,_,_),_ =
-    intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
+    intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None)
       {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
       (vars, Id.Map.empty) None [] r
@@ -990,10 +991,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,[]) in (b,(Loc.tag @@ RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,l) in (b,(Loc.tag @@ RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1239,7 +1240,7 @@ let drop_notations_pattern looked_for =
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
-	      if List.length pats < nvars then error_not_enough_arguments loc;
+	      if List.length pats < nvars then error_not_enough_arguments ~loc;
 	      let pats1,pats2 = List.chop nvars pats in
 	      let subst = make_subst vars pats1 in
 	      let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in
@@ -1288,20 +1289,20 @@ let drop_notations_pattern looked_for =
         Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
-      fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+      fst (Notation.interp_prim_token_cases_pattern_expr ~loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (ntn, fullargs,extrargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
-      let ((ids',c),df) = Notation.interp_notation loc ntn scopes in
+      let ((ids',c),df) = Notation.interp_notation ~loc ntn scopes in
       let (ids',idsl',_) = split_by_type ids' in
       Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let substlist = make_subst idsl' argsl in
       let subst = make_subst ids' args in
       in_not top loc scopes (subst,substlist) extrargs c
     | CPatDelimiters (key, e) ->
-      in_pat top (None,find_delimiters_scope loc key::snd scopes) e
-    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+      in_pat top (None,find_delimiters_scope ~loc key::snd scopes) e
+    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ~loc (test_kind false) p scopes)
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
@@ -1540,7 +1541,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	       let before, after = split_at_annot bl n in
 	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
 	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.count (function GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in
+	       let n' = Option.map (fun _ -> List.count (function | _, GLocalAssum _ -> true
+                                                                  | _ -> false (* remove let-ins *))
+                        rbefore) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, (env',rbl) =
@@ -1559,7 +1562,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
-					    en (Loc.ghost, Name name)) 0 env' lf in
+					    en (Loc.tag @@ Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	Loc.tag ~loc @@
           GRec (GFix
@@ -1586,7 +1589,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
-					    en (Loc.ghost, Name name)) 0 env' lf in
+					    en (Loc.tag @@ Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	Loc.tag ~loc @@
 	GRec (GCoFix n,
@@ -1617,10 +1620,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CGeneralization (b,a,c) ->
         intern_generalization intern env ntnvars loc b a c
     | CPrim p ->
-	fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
+	fst (Notation.interp_prim_token ~loc p (env.tmp_scope,env.scopes))
     | CDelimiters (key, e) ->
 	intern {env with tmp_scope = None;
-		  scopes = find_delimiters_scope loc key :: env.scopes} e
+		  scopes = find_delimiters_scope ~loc key :: env.scopes} e
     | CAppExpl ((isproj,ref,us), args) ->
         let (f,_,args_scopes,_),args =
 	  let args = List.map (fun a -> (a,None)) args in
@@ -1679,7 +1682,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
 	  tms ([],Id.Set.empty,[]) in
         let env' = Id.Set.fold
-	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var))
+	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.tag @@ Name var))
 	  (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
@@ -1715,7 +1718,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
-	    (Loc.ghost,na') in
+	    (Loc.tag na') in
 	  intern_type env'' u) po in
 	Loc.tag ~loc @@
         GLetTuple (List.map snd nal, (na', p'), b',
@@ -1725,7 +1728,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       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 ->
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
-	    (Loc.ghost,na') in
+	    (Loc.tag na') in
 	  intern_type env'' p) po in
 	Loc.tag ~loc @@
         GIf (c', (na', p'), intern env b1, intern env b2)
@@ -1779,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   )
   and intern_type env = intern (set_type_scope env)
 
-  and intern_local_binder env bind =
+  and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
     intern_local_binder_aux intern ntnvars env bind
 
   (* Expands a multiple pattern into a disjunction of multiple patterns *)
@@ -1815,7 +1818,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     let extra_id,na = match tm', na with
       | (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)
+      | _, None -> None,(Loc.tag Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
     (* the "in" part *)
     let match_td,typ = match t with
@@ -1837,7 +1840,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
-		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
+		canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
 	      | _::t, (loc, PatVar x)::tt ->
@@ -2052,12 +2055,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
 
 let interp_binder env sigma na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole (loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
   understand ~expected_type:IsType env sigma t'
 
 let interp_binder_evars env evdref na t =
   let t = intern_gen IsType env t in
-  let t' = locate_if_hole (loc_of_glob_constr t) na t in
+  let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
 open Environ
@@ -2084,7 +2087,7 @@ let interp_rawcontext_evars env evdref k bl =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
        let t' =
-	 if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t
+	 if Option.is_empty b then locate_if_hole ~loc:(loc_of_glob_constr t) na t
 	 else t
        in
        let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 51152bb24e..fa7712bdcb 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -252,7 +252,7 @@ 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
-      (Loc.tag @@ CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
+      (Loc.tag @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid)
 
 let destClassApp (loc, cl) =
   match cl with
diff --git a/interp/notation.ml b/interp/notation.ml
index 3bcec30012..150be040f3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -220,10 +220,10 @@ let remove_delimiters scope =
        with Not_found ->
          assert false (* A delimiter for scope [scope] should exist *)
 
-let find_delimiters_scope loc key =
+let find_delimiters_scope ?loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
-    user_err ~loc ~hdr:"find_delimiters"
+    user_err ?loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
@@ -291,7 +291,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 type required_module = full_path * string list
 
 type 'a prim_token_interpreter =
-    Loc.t -> 'a -> glob_constr
+    ?loc:Loc.t -> 'a -> glob_constr
 
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
@@ -299,7 +299,7 @@ type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
 
 type internal_prim_token_interpreter =
-    Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+    ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
 
 let prim_token_interpreter_tab =
   (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -309,7 +309,7 @@ let add_prim_token_interpreter sc interp =
     let cont = Hashtbl.find prim_token_interpreter_tab sc in
     Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
   with Not_found ->
-    let cont = (fun _loc _p -> raise Not_found) in
+    let cont = (fun ?loc _p -> raise Not_found) in
     Hashtbl.add prim_token_interpreter_tab sc (interp cont)
 
 let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
@@ -325,22 +325,22 @@ let mkString = function
 | None -> None
 | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
-let delay dir int loc x = (dir, (fun () -> int loc x))
+let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
 
 let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+    (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
     (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
 
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
-    (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+    (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
     (patl, (fun r -> mkString (uninterp r)), inpat)
 
-let check_required_module loc sc (sp,d) =
+let check_required_module ?loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ~loc ~hdr:"prim_token_interpreter"
+    user_err ?loc ~hdr:"prim_token_interpreter"
     (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
@@ -445,23 +445,23 @@ let notation_of_prim_token = function
   | Numeral n -> "- "^(to_string (neg n))
   | String _ -> raise Not_found
 
-let find_prim_token g loc p sc =
+let find_prim_token ?loc g p sc =
   (* Try for a user-defined numerical notation *)
   try
     let (_,c),df = find_notation (notation_of_prim_token p) sc in
-    g (Notation_ops.glob_constr_of_notation_constr loc c),df
+    g (Notation_ops.glob_constr_of_notation_constr ?loc c),df
   with Not_found ->
   (* Try for a primitive numerical notation *)
-  let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
-  check_required_module loc sc spdir;
+  let (spdir,interp) = (Hashtbl.find prim_token_interpreter_tab sc) ?loc p in
+  check_required_module ?loc sc spdir;
   g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
 
-let interp_prim_token_gen g loc p local_scopes =
+let interp_prim_token_gen g ?loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
-  try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
+  try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
   with Not_found ->
-    user_err ~loc ~hdr:"interp_prim_token"
+    user_err ?loc ~hdr:"interp_prim_token"
     ((match p with
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
@@ -480,14 +480,14 @@ let rec rcp_of_glob looked_for gt = Loc.map (function
   | _ -> 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
+let interp_prim_token_cases_pattern_expr ?loc looked_for p =
+  interp_prim_token_gen (rcp_of_glob looked_for) ?loc p
 
-let interp_notation loc ntn local_scopes =
+let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
-    user_err ~loc 
+    user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
@@ -541,7 +541,7 @@ let uninterp_prim_token_cases_pattern c =
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
-    try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true
+    try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
     with Not_found -> false in
   let scopes = make_current_scopes local_scopes in
   Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -823,7 +823,7 @@ let pr_scope_classes sc =
 
 let pr_notation_info prglob ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++
-  prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
+  prglob (Notation_ops.glob_constr_of_notation_constr c)
 
 let pr_named_scope prglob scope sc =
  (if String.equal scope default_scope then
@@ -891,25 +891,25 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
       Some (ntn,sc,ref)
   | _ -> None
 
-let error_ambiguous_notation loc _ntn =
-  user_err ~loc  (str "Ambiguous notation.")
+let error_ambiguous_notation ?loc _ntn =
+  user_err ?loc (str "Ambiguous notation.")
 
-let error_notation_not_reference loc ntn =
-  user_err ~loc 
+let error_notation_not_reference ?loc ntn =
+  user_err ?loc 
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
-let interp_notation_as_global_reference loc test ntn sc =
+let interp_notation_as_global_reference ?loc test ntn sc =
   let scopes = match sc with
   | Some sc ->
-      let scope = find_scope (find_delimiters_scope Loc.ghost sc) in
+      let scope = find_scope (find_delimiters_scope sc) in
       String.Map.add sc scope String.Map.empty
   | None -> !scope_map in
   let ntns = browse_notation true ntn scopes in
   let refs = List.map (global_reference_of_notation test) ntns in
   match Option.List.flatten refs with
   | [_,_,ref] -> ref
-  | [] -> error_notation_not_reference loc ntn
+  | [] -> error_notation_not_reference ?loc ntn
   | refs ->
       let f (ntn,sc,ref) =
         let def = find_default ntn !scope_stack in
@@ -919,8 +919,8 @@ let interp_notation_as_global_reference loc test ntn sc =
       in
       match List.filter f refs with
       | [_,_,ref] -> ref
-      | [] -> error_notation_not_reference loc ntn
-      | _ -> error_ambiguous_notation loc ntn
+      | [] -> error_notation_not_reference ?loc ntn
+      | _ -> error_ambiguous_notation ?loc ntn
 
 let locate_notation prglob ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in
diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..10c7b85e4e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,7 +55,7 @@ val find_scope : scope_name -> scope
 
 val declare_delimiters : scope_name -> delimiters -> unit
 val remove_delimiters : scope_name -> unit
-val find_delimiters_scope : Loc.t -> delimiters -> scope_name
+val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
@@ -69,7 +69,7 @@ type required_module = full_path * string list
 type cases_pattern_status = bool (** true = use prim token in patterns *)
 
 type 'a prim_token_interpreter =
-    Loc.t -> 'a -> glob_constr
+    ?loc:Loc.t -> 'a -> glob_constr
 
 type 'a prim_token_uninterpreter =
     glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
@@ -83,9 +83,9 @@ val declare_string_interpreter : scope_name -> required_module ->
 (** Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
+val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
-val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
   local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
@@ -114,7 +114,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (** Return the interpretation bound to a notation *)
-val interp_notation : Loc.t -> notation -> local_scopes ->
+val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
 type notation_rule = interp_rule * interpretation * int option
@@ -137,7 +137,7 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
 
 (** {6 Miscellaneous} *)
 
-val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
+val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
       notation -> delimiters option -> global_reference
 
 (** Checks for already existing notations *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 32c900504b..32c5641566 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -117,13 +117,13 @@ let name_to_ident = function
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
-let rec cases_pattern_fold_map loc g e = Loc.with_unloc (function
+let rec cases_pattern_fold_map ?loc g e = Loc.with_unloc (function
   | PatVar na ->
-      let e',na' = g e na in e', Loc.tag ~loc @@ PatVar na'
+      let e',na' = g e na in e', Loc.tag ?loc @@ PatVar na'
   | PatCstr (cstr,patl,na) ->
       let e',na' = g e na in
-      let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
-      e', Loc.tag ~loc @@ PatCstr (cstr,patl',na')
+      let e',patl' = List.fold_map (cases_pattern_fold_map ?loc g) e patl in
+      e', Loc.tag ?loc @@ PatCstr (cstr,patl',na')
   )
 
 let subst_binder_type_vars l = function
@@ -152,8 +152,8 @@ let rec subst_glob_vars l gc = Loc.map (function
 
 let ldots_var = Id.of_string ".."
 
-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
+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) ->
@@ -181,13 +181,13 @@ let glob_constr_of_notation_constr_with_binders loc g f e nc =
 	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
 	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (loc,(ind,nal')) in
+	  e',Some (Loc.tag ?loc (ind,nal')) in
 	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
-	  List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
+	  List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
 	lt (idl,patl,f e rhs)) eqnl in
       GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
@@ -208,9 +208,9 @@ let glob_constr_of_notation_constr_with_binders loc g f e nc =
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
 
-let glob_constr_of_notation_constr loc x =
+let glob_constr_of_notation_constr ?loc x =
   let rec aux () x =
-    glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
+    glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x
   in aux () x
 
 (******************************************************************************)
@@ -795,17 +795,17 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
       | (Some _ as x), None | None, (Some _ as x) -> x
       | None, None -> None in
     let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
-    let unify_binder alp b b' =
+    let unify_binder alp (loc, b) (loc', b') =
       match b, b' with
-      | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') ->
+      | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
          let alp, na = unify_name alp na na' in
-         alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t')
-      | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') ->
+         alp, Loc.tag ~loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+      | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
          let alp, na = unify_name alp na na' in
-         alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
-      | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') ->
+         alp, Loc.tag ~loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+      | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
          let alp, p = unify_pat alp p p' in
-         alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+         alp, Loc.tag ~loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -832,18 +832,18 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
     let unify_pat p p' =
       if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
       else raise No_match in
-    let unify_term_binder c b' =
+    let unify_term_binder c (loc, b') = Loc.tag ~loc @@
       match c, b' with
-      | (_, GVar id), GLocalAssum (loc, na', bk', t') ->
-         GLocalAssum (loc, unify_id id na', bk', t')
-      | c, GLocalPattern (loc, (p',ids), id, bk', t') ->
+      | (_, GVar id), GLocalAssum (na', bk', t') ->
+         GLocalAssum (unify_id id na', bk', t')
+      | c, GLocalPattern ((p',ids), id, bk', t') ->
          let p = pat_binder_of_term c in
-         GLocalPattern (loc, (unify_pat p p',ids), id, bk', t')
+         GLocalPattern ((unify_pat p p',ids), id, bk', t')
       | _ -> raise No_match in
     let rec unify cl bl' =
     match cl, bl' with
     | [], [] -> []
-    | c :: cl, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl'
+    | c :: cl, (_loc, GLocalDef ( _, _, _, t)) :: bl' -> unify cl bl'
     | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
     | _ -> raise No_match in
     let bl = unify cl bl' in
@@ -898,17 +898,17 @@ let glue_letin_with_decls = true
 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
+      match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalPattern((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
+      match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalAssum(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
+      match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalPattern((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
+      match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalAssum(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
+	((Loc.tag ~loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
   | b -> (decls, Loc.tag ~loc b)
   ) bi
 
@@ -989,13 +989,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
   (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
   | 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 (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalPattern((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 (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
+      let (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalAssum (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
@@ -1003,13 +1003,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
   (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
   | 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 (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalPattern ((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 (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
+      let (decls,b) = match_iterated_binders false [Loc.tag ~loc @@ GLocalAssum (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
@@ -1021,15 +1021,15 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | 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
+      let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
       match_in u alp metas sigma b1 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
+      let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalAssum (na,bk,t)] in
       match_in u alp metas sigma b1 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
+      let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalAssum (na,bk,t)] in
       match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
@@ -1121,10 +1121,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)]
+          bind_bindinglist_env alp sigma id [Loc.tag @@ GLocalAssum (Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
-      match_in u alp metas sigma (mkGApp Loc.ghost a1 (Loc.tag @@ GVar id')) b2
+      match_in u alp metas sigma (mkGApp a1 (Loc.tag @@ GVar id')) b2
 
   | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index a61ba172ee..64f811dc20 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -33,12 +33,12 @@ val notation_constr_of_glob_constr : notation_interp_env ->
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
-val glob_constr_of_notation_constr_with_binders : Loc.t ->
+val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
   ('a -> Name.t -> 'a * Name.t) ->
   ('a -> notation_constr -> glob_constr) ->
   'a -> notation_constr -> glob_constr
 
-val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
+val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_constr
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)
 
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 64d260cc1b..fd9599ec02 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -67,14 +67,14 @@ let smart_global ?head = function
   | AN r ->
       global_with_alias ?head r
   | ByNotation (loc,(ntn,sc)) ->
-      Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
+      Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc
 
 let smart_global_inductive = function
   | AN r ->
       global_inductive_with_alias r
   | ByNotation (loc,(ntn,sc)) ->
       destIndRef
-        (Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
+        (Notation.interp_notation_as_global_reference ~loc isIndRef ntn sc)
 
 let loc_of_smart_reference = function
   | AN r -> loc_of_reference r
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c8fbdaf285..2ffeb1f83d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -282,7 +282,7 @@ let locs_of_notation loc locs ntn =
 let ntn_loc loc (args,argslist,binderslist) =
   locs_of_notation loc
     (List.map constr_loc (args@List.flatten argslist)@
-     List.map local_binders_loc binderslist)
+     List.map_filter local_binders_loc binderslist)
 
 let patntn_loc loc (args,argslist) =
   locs_of_notation loc