[location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.

18 files changed, 152 insertions, 152 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index d6a334c5fe..0cdb10a378 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -892,7 +892,7 @@ let extract_constant_inline inline r ids s =
 let extract_inductive r s l optstr =
   check_inside_section ();
   let g = Smartlocate.global_with_alias r in
-  Dumpglob.add_glob (loc_of_reference r) g;
+  Dumpglob.add_glob ?loc:(loc_of_reference r) g;
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 129c8dc165..ee82d95d09 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -159,7 +159,7 @@ GEXTEND Gram
   GLOBAL: function_rec_definition_loc ;
 
   function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> !@loc, g ]]
+    [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]]
     ;
 
 END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 946ee55d46..48ab3dd57c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -610,7 +610,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
-        let v = match typ with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in
+        let v = match typ with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -973,7 +973,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      Loc.tag ~loc:loc1 @@ GApp(Loc.tag ~loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ~loc:loc3 @@ GVar id;rt_typ;rt])
+		      Loc.tag ?loc:loc1 @@ GApp(Loc.tag ?loc:loc2 @@GRef(jmeq,None),[ty;Loc.tag ?loc:loc3 @@ GVar id;rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
@@ -1119,7 +1119,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	end
     | loc, GLetIn(n,v,t,b) ->
 	begin
-          let t = match t with None -> v | Some t -> Loc.tag ~loc @@ GCast (v,CastConv t) in
+          let t = match t with None -> v | Some t -> Loc.tag ?loc @@ GCast (v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1249,11 +1249,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_
 let rec rebuild_return_type (loc, rt) =
   match rt with
     | Constrexpr.CProdN(n,t') ->
-        Loc.tag ~loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
+        Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
-	Loc.tag ~loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> Loc.tag ~loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
-				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ~loc rt],
+	Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+    | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt],
 			    Loc.tag @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 01e607412a..66b9897d04 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -193,14 +193,14 @@ let rec alpha_pat excluded (loc, pat) =
   match pat with
     | PatVar Anonymous ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	(Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+	(Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
     | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
-	  (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),
+	  (Loc.tag ?loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
-	else (Loc.tag ~loc pat),excluded,Id.Map.empty
+	else (Loc.tag ?loc pat),excluded,Id.Map.empty
     | PatCstr(constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
@@ -218,7 +218,7 @@ let rec alpha_pat excluded (loc, pat) =
 	    ([],new_excluded,map)
 	    patl
 	in
-        (Loc.tag ~loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
+        (Loc.tag ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
 
 let alpha_patl excluded patl  =
   let patl,new_excluded,map =
@@ -255,7 +255,7 @@ let raw_get_pattern_id pat acc =
 let get_pattern_id pat = raw_get_pattern_id pat []
 
 let rec alpha_rt excluded (loc, rt) =
-  let new_rt = Loc.tag ~loc @@
+  let new_rt = Loc.tag ?loc @@
     match rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
       | GLambda(Anonymous,k,t,b) ->
@@ -445,7 +445,7 @@ let rec pattern_to_term pt = Loc.with_unloc (function
 
 
 let replace_var_by_term x_id term =
-  let rec replace_var_by_pattern (loc, rt) = Loc.tag ~loc @@
+  let rec replace_var_by_pattern (loc, rt) = Loc.tag ?loc @@
     match rt with
       | GRef _ -> rt
       | GVar id when Id.compare id x_id == 0 -> Loc.obj term
@@ -605,7 +605,7 @@ let ids_of_glob_constr c =
 
 
 let zeta_normalize =
-  let rec zeta_normalize_term (loc, rt) = Loc.tag ~loc @@
+  let rec zeta_normalize_term (loc, rt) = Loc.tag ?loc @@
     match rt with
       | GRef _ -> rt
       | GVar _ -> rt
@@ -673,7 +673,7 @@ let expand_as =
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map (loc, rt) =
-    Loc.tag ~loc @@
+    Loc.tag ?loc @@
     match rt with
       | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> rt
       | GVar id ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1da85c467a..3dc16626ce 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -756,7 +756,7 @@ let rec add_args id new_args = Loc.map (function
 	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
 			 na, b_option) cel,
-	     List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc @@ (cpl,add_args id new_args e)) cal
+	     List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(nal,(na,b_option),b1,b2) ->
       CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
@@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) -> Loc.tag ~loc @@ 
+					(fun (loc,n) -> Loc.tag ?loc @@ 
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 5123d6c403..dc43930e4d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -267,7 +267,7 @@ let add_rewrite_hint bases ort t lcsr =
 	  (Declare.declare_universe_context false ctx;
            Univ.ContextSet.empty)
     in
-      Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in
+      Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
   let eqs = List.map f lcsr in
   let add_hints base = add_rew_rules base eqs in
   List.iter add_hints bases
@@ -679,8 +679,8 @@ let hResolve id c occ t =
     with
       | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
           let (e, info) = CErrors.push e in
-          let loc = match Loc.get_loc info with None -> 0,0 | Some loc -> Loc.unloc loc in
-          resolve_hole (subst_hole_with_term (fst loc) c_raw t_hole)
+          let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in
+          resolve_hole (subst_hole_with_term loc_begin c_raw t_hole)
   in
   let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr = EConstr.of_constr t_constr in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 23643c5d34..e20beae963 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -41,7 +41,7 @@ let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
   | Libnames.Qualid (loc,_) ->
-      CErrors.user_err ~loc 
+      CErrors.user_err ?loc 
        (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
@@ -159,9 +159,9 @@ GEXTEND Gram
       | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ];
 	  l = LIST0 message_token -> TacFail (g,n,l)
       | st = simple_tactic -> st
-      | a = tactic_arg -> TacArg(!@loc,a)
+      | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a)
       | r = reference; la = LIST0 tactic_arg_compat ->
-          TacArg(!@loc, TacCall (!@loc,(r,la))) ]
+          TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
       | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
@@ -169,7 +169,7 @@ GEXTEND Gram
           | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
           | None -> TacDispatch tf
           end
-      | a = tactic_atom -> TacArg (!@loc,a) ] ]
+      | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ]
   ;
   failkw:
   [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ]
@@ -203,7 +203,7 @@ GEXTEND Gram
      verbose most of the time. *)
   fresh_id:
     [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
-	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (!@loc,id) ] ]
+	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -219,7 +219,7 @@ GEXTEND Gram
   ;
   tactic_atom:
     [ [ n = integer -> TacGeneric (genarg_of_int n)
-      | r = reference -> TacCall (!@loc,(r,[]))
+      | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[]))
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
   match_key:
@@ -470,7 +470,7 @@ let pr_ltac_production_item = function
 VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
 | [ string(s) ] -> [ Tacentries.TacTerm s ]
 | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
-  [ Tacentries.TacNonTerm (loc, ((Names.Id.to_string nt, sep), p)) ]
+  [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), p)) ]
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index d1e5c810f4..8aaad05666 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -166,20 +166,20 @@ let mkTacCase with_evar = function
 	error "Use of numbers as direct arguments of 'case' is not supported.";
       TacInductionDestruct (false,with_evar,ic)
 
-let rec mkCLambdaN_simple_loc loc bll c =
+let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      Loc.tag ~loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
-  | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
+      Loc.tag ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+  | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
 
 let mkCLambdaN_simple bl c = match bl with
   | [] -> c
   | h :: _ ->
-    let loc = Loc.merge (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
-    mkCLambdaN_simple_loc loc bl c
+    let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
+    mkCLambdaN_simple_loc ?loc bl c
 
-let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l))
+let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 let map_int_or_var f = function
   | ArgArg x -> ArgArg (f x)
@@ -301,7 +301,7 @@ GEXTEND Gram
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function
 	    | ([]|[_]|[_;_]) as l -> l
-	    | t::q -> [t;(loc_of_ne_list q,IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+	    | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
 	  in IntroAndPattern (pairify (si::tc)) ] ]
   ;
   equality_intropattern:
@@ -316,8 +316,8 @@ GEXTEND Gram
   ;
   nonsimple_intropattern:
     [ [ l = simple_intropattern -> l
-      | "*" -> !@loc, IntroForthcoming true
-      | "**" -> !@loc, IntroForthcoming false ]]
+      | "*"  -> Loc.tag ~loc:!@loc @@ IntroForthcoming true
+      | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]]
   ;
   simple_intropattern:
     [ [ pat = simple_intropattern_closed;
@@ -325,15 +325,15 @@ GEXTEND Gram
           let loc0,pat = pat in
           let f c pat =
             let loc1 = Constrexpr_ops.constr_loc c in
-            let loc = Loc.merge loc0 loc1 in
+            let loc = Loc.merge_opt loc0 loc1 in
             IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
-          !@loc, List.fold_right f l pat ] ]
+          Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ]
   ;
   simple_intropattern_closed:
-    [ [ pat = or_and_intropattern -> !@loc, IntroAction (IntroOrAndPattern pat)
-      | pat = equality_intropattern -> !@loc, IntroAction pat
-      | "_" -> !@loc, IntroAction IntroWildcard 
-      | pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
+    [ [ pat = or_and_intropattern   -> Loc.tag ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
+      | pat = equality_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction pat
+      | "_" -> Loc.tag ~loc:!@loc @@ IntroAction IntroWildcard 
+      | pat = naming_intropattern -> Loc.tag ~loc:!@loc @@ IntroNaming pat ] ]
   ;
   simple_binding:
     [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c)
@@ -468,7 +468,7 @@ GEXTEND Gram
       | -> None ] ]
   ;
   or_and_intropattern_loc:
-    [ [ ipat = or_and_intropattern -> ArgArg (!@loc,ipat)
+    [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat)
       | locid = identref -> ArgVar locid ] ]
   ;
   as_or_and_ipat:
@@ -476,13 +476,13 @@ GEXTEND Gram
       | -> None ] ]
   ;
   eqn_ipat:
-    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (!@loc, pat)
+    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
          let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "H"; Some (loc, pat)
+	 warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat)
       | IDENT "_eqn" ->
          let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "?"; Some (loc, IntroAnonymous)
+	 warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
@@ -521,145 +521,145 @@ GEXTEND Gram
     [ [
       (* Basic tactics *)
         IDENT "intros"; pl = ne_intropatterns ->
-          TacAtom (!@loc, TacIntroPattern (false,pl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
       | IDENT "intros" ->
-          TacAtom (!@loc, TacIntroPattern (false,[!@loc,IntroForthcoming false]))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false]))
       | IDENT "eintros"; pl = ne_intropatterns ->
-          TacAtom (!@loc, TacIntroPattern (true,pl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,false,cl,inhyp))
+          inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp))
       | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (true,true,cl,inhyp))
+          inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp))
       | IDENT "simple"; IDENT "apply";
           cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,false,cl,inhyp))
+          inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp))
       | IDENT "simple"; IDENT "eapply";
           cl = LIST1 constr_with_bindings_arg SEP",";
-          inhyp = in_hyp_as -> TacAtom (!@loc, TacApply (false,true,cl,inhyp))
+          inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp))
       | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          TacAtom (!@loc, TacElim (false,cl,el))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el))
       | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          TacAtom (!@loc, TacElim (true,cl,el))
-      | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl)
-      | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl)
+          TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el))
+      | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl)
+      | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl)
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
-	  TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd))
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
-	  TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacAtom (!@loc, TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
       | IDENT "pose"; b = constr; na = as_name ->
-	  TacAtom (!@loc, TacLetTac (na,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None))
       | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
-	  TacAtom (!@loc, TacLetTac (Names.Name id,c,p,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None))
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
-          TacAtom (!@loc, TacLetTac (na,c,p,true,None))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None))
       | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          TacAtom (!@loc, TacLetTac (na,c,p,false,e))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e))
 
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (!@loc, TacAssert (true,None,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (!@loc, TacAssert (true,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "enough c as id by tac" *)
       | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (!@loc, TacAssert (false,Some tac,Some (!@loc,IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (!@loc, TacAssert (true,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAtom (!@loc, TacAssert (true,None,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (!@loc, TacAssert (false,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
 
       | IDENT "generalize"; c = constr ->
-	  TacAtom (!@loc, TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
 	  let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
-          TacAtom (!@loc, TacGeneralize (List.map gen_everywhere (c::l)))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l)))
       | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
           na = as_name;
           l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
-          TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l))
 
       (* Derived basic tactics *)
       | IDENT "induction"; ic = induction_clause_list ->
-	  TacAtom (!@loc, TacInductionDestruct (true,false,ic))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic))
       | IDENT "einduction"; ic = induction_clause_list ->
-	  TacAtom (!@loc, TacInductionDestruct(true,true,ic))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic))
       | IDENT "destruct"; icl = induction_clause_list ->
-	  TacAtom (!@loc, TacInductionDestruct(false,false,icl))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl))
       | IDENT "edestruct";  icl = induction_clause_list ->
-	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl))
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t))
       | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=by_tactic -> TacAtom (!@loc, TacRewrite (true,l,cl,t))
+	  cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t))
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> SimpleInversion
 	  | IDENT "inversion" -> FullInversion
 	  | IDENT "inversion_clear" -> FullInversionClear ];
 	  hyp = quantified_hypothesis;
 	  ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] ->
-	    TacAtom (!@loc, TacInversion (DepInversion (k,co,ids),hyp))
+	    TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp))
       | IDENT "simple"; IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    TacAtom (!@loc, TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
+	    TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp))
       | IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    TacAtom (!@loc, TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
+	    TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp))
       | IDENT "inversion_clear";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    TacAtom (!@loc, TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
+	    TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp))
       | IDENT "inversion"; hyp = quantified_hypothesis;
 	  "using"; c = constr; cl = in_hyp_list ->
-	    TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
+	    TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp))
 
       (* Conversion *)
       | IDENT "red"; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Red false, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl))
       | IDENT "hnf"; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Hnf, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl))
       | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl))
       | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Cbv s, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl))
       | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Cbn s, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl))
       | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Lazy s, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl))
       | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl))
       | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (CbvVm po, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl))
       | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (CbvNative po, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl))
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Unfold ul, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl))
       | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Fold l, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl))
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
-          TacAtom (!@loc, TacReduce (Pattern pl, cl))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl))
 
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
 	  let p,cl = merge_occurrences (!@loc) cl oc in
-	  TacAtom (!@loc, TacChange (p,c,cl))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl))
     ] ]
   ;
 END;;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 26ac3c53e3..bdafbdc78c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -352,7 +352,7 @@ type 'a extra_genarg_printer =
 
   let pr_ltac_or_var pr = function
     | ArgArg x -> pr x
-    | ArgVar (loc,id) -> pr_with_comments ~loc (pr_id id)
+    | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
 
   let pr_ltac_constant kn =
     if !Flags.in_debugger then pr_kn kn
@@ -507,7 +507,7 @@ type 'a extra_genarg_printer =
 
   let pr_core_destruction_arg prc prlc = function
     | ElimOnConstr c -> pr_with_bindings prc prlc c
-    | ElimOnIdent (loc,id) -> pr_with_comments ~loc (pr_id id)
+    | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id)
     | ElimOnAnonHyp n -> int n
 
   let pr_destruction_arg prc prlc (clear_flag,h) =
@@ -1037,7 +1037,7 @@ type 'a extra_genarg_printer =
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom (loc,t) ->
-              pr_with_comments ~loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
+              pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
             | TacArg(_,Tacexp e) ->
               pr.pr_tactic (latom,E) e, latom
             | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1051,16 +1051,16 @@ type 'a extra_genarg_printer =
             | TacArg(_,TacCall(loc,(f,[]))) ->
               pr.pr_reference f, latom
             | TacArg(_,TacCall(loc,(f,l))) ->
-              pr_with_comments ~loc (hov 1 (
+              pr_with_comments ?loc (hov 1 (
                 pr.pr_reference f ++ spc ()
                 ++ prlist_with_sep spc pr_tacarg l)),
               lcall
             | TacArg (_,a) ->
               pr_tacarg a, latom
             | TacML (loc,(s,l)) ->
-              pr_with_comments ~loc (pr.pr_extend 1 s l), lcall
+              pr_with_comments ?loc (pr.pr_extend 1 s l), lcall
             | TacAlias (loc,(kn,l)) ->
-              pr_with_comments ~loc (pr.pr_alias (level_of inherited) kn l), latom
+              pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom
           )
           in
           if prec_less prec inherited then strm
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index b76009c997..e037bb4b26 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -268,11 +268,11 @@ let coerce_to_constr_list env v =
     List.map map l
   | None -> raise (CannotCoerceTo "a term list")
 
-let coerce_to_intro_pattern_list loc env sigma v =
+let coerce_to_intro_pattern_list ?loc env sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = (loc, coerce_to_intro_pattern env sigma v) in
+    let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in
     List.map map l
 
 let coerce_to_hyp env sigma v =
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9c4ac52657..b09672a12b 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -76,7 +76,7 @@ val coerce_to_evaluable_ref :
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
 val coerce_to_intro_pattern_list :
-  Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
+  ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
 
 val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f608515aa7..a19dbd3276 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
         TacGeneric arg
     in
     let l = List.map map l in
-    (TacAlias (loc,(kn,l)):raw_tactic_expr)
+    (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr)
   in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
@@ -180,6 +180,7 @@ let add_tactic_entry (kn, ml, tg) state =
   | TacTerm s -> GramTerminal s
   | TacNonTerm (loc, (s, _)) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
+    let loc = Option.default Loc.internal_ghost loc in
     GramNonTerminal (loc, typ, e)
   in
   let prods = List.map map tg.tacgram_prods in
@@ -405,7 +406,7 @@ let create_ltac_quotation name cast (e, l) =
       entry),
       Atoken (CLexer.terminal ")"))
   in
-  let action _ v _ _ _ loc = cast (loc, v) in
+  let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in
   Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
 
@@ -431,7 +432,7 @@ let register_ltac local tacl =
         let kn = Lib.make_kn id in
         let id_pp = pr_id id in
         let () = if is_defined_tac kn then
-          CErrors.user_err ~loc 
+          CErrors.user_err ?loc 
             (str "There is already an Ltac named " ++ id_pp ++ str".")
         in
         let is_shadowed =
@@ -448,7 +449,7 @@ let register_ltac local tacl =
         let kn =
           try Nametab.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
-            CErrors.user_err ~loc 
+            CErrors.user_err ?loc 
                        (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
         in
         UpdateTac kn, body
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 787a5f50bd..44ea3ff1d6 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -72,7 +72,7 @@ let intern_name l ist = function
 
 let strict_check = ref false
 
-let adjust_loc loc = if !strict_check then None else Some loc
+let adjust_loc loc = if !strict_check then None else loc
 
 (* Globalize a name which must be bound -- actually just check it is bound *)
 let intern_hyp ist (loc,id as locid) =
@@ -81,7 +81,7 @@ let intern_hyp ist (loc,id as locid) =
   else if find_ident id ist then
     Loc.tag id
   else
-    Pretype_errors.error_var_not_found ~loc id
+    Pretype_errors.error_var_not_found ?loc id
 
 let intern_or_var f ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
@@ -126,7 +126,7 @@ let intern_move_location ist = function
 
 let intern_isolated_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  TacCall (Loc.tag ~loc (ArgArg (loc,locate_tactic qid),[]))
+  TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[]))
 
 let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
@@ -293,7 +293,7 @@ let intern_evaluable_reference_or_by_notation ist = function
   | AN r -> intern_evaluable_global_reference ist r
   | ByNotation (loc,(ntn,sc)) ->
       evaluable_of_global_reference ist.genv
-      (Notation.interp_notation_as_global_reference ~loc
+      (Notation.interp_notation_as_global_reference ?loc
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
@@ -372,13 +372,13 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
 let dump_glob_red_expr = function
   | Unfold occs -> List.iter (fun (_, r) ->
     try
-      Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
+      Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
 	(Smartlocate.smart_global r)
     with e when CErrors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
-        Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
+        Dumpglob.add_glob ?loc:(loc_of_or_by_notation Libnames.loc_of_reference r)
 	  (Smartlocate.smart_global r)
       with e when CErrors.noncritical e -> ()) grf.rConst
   | _ -> ()
@@ -459,7 +459,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 (* Utilities *)
 let extract_let_names lrc =
   let fold accu ((loc, name), _) =
-    if Id.Set.mem name accu then user_err ~loc
+    if Id.Set.mem name accu then user_err ?loc
       ~hdr:"glob_tactic" (str "This variable is bound several times.")
     else Id.Set.add name accu
   in
@@ -626,7 +626,7 @@ and intern_tactic_seq onlytac ist = function
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
       let l = List.map (intern_tacarg !strict_check false ist) l in
-      ist.ltacvars, TacAlias (Loc.tag ~loc (s,l))
+      ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
   | TacML (loc,(opn,l)) ->
       let _ignore = Tacenv.interp_ml_tactic opn in
       ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l))
@@ -637,7 +637,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
   | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
-      if onlytac then error_tactic_expected ~loc else TacArg (loc,a)
+      if onlytac then error_tactic_expected ?loc else TacArg (loc,a)
 
 and intern_tactic_or_tacarg ist = intern_tactic false ist
 
@@ -652,7 +652,7 @@ and intern_tacarg strict onlytac ist = function
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
   | TacCall (loc,(f,l)) ->
-      TacCall (Loc.tag ~loc (
+      TacCall (Loc.tag ?loc (
         intern_applied_tactic_reference ist f,
         List.map (intern_tacarg !strict_check false ist) l))
   | TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index e969b86f6f..4d5b844550 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -313,7 +313,7 @@ let append_trace trace v =
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id v =
   let v = Value.normalize v in
-  let fail () = user_err ~loc 
+  let fail () = user_err ?loc 
     (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
   in
   let v = Value.normalize v in
@@ -376,7 +376,7 @@ let error_ltac_variable ?loc id env v s =
 (* Raise Not_found if not in interpretation sign *)
 let try_interp_ltac_var coerce ist env (loc,id) =
   let v = Id.Map.find id ist.lfun in
-  try coerce v with CannotCoerceTo s -> error_ltac_variable ~loc id env v s
+  try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
@@ -402,7 +402,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
-    user_err ~loc:(fst locid) ~hdr:"interp_int"
+    user_err ?loc:(fst locid) ~hdr:"interp_int"
      (str "Unbound variable "  ++ pr_id (snd locid) ++ str".")
 
 let interp_int_or_var ist = function
@@ -425,7 +425,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
+  else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env sigma (loc,id as x) =
   try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
@@ -447,7 +447,7 @@ let interp_reference ist env sigma = function
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
-      with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
 
 let try_interp_evaluable env (loc, id) =
   let v = Environ.lookup_named id env in
@@ -463,14 +463,14 @@ let interp_evaluable ist env sigma = function
       with Not_found ->
         match r with
         | EvalConstRef _ -> r
-        | _ -> error_global_not_found ~loc (qualid_of_ident id)
+        | _ -> error_global_not_found ?loc (qualid_of_ident id)
     end
   | ArgArg (r,None) -> r
   | ArgVar (loc, id) ->
     try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
-      with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
+      with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
 
 (* Interprets an hypothesis name *)
 let interp_occurrences ist occs =
@@ -739,7 +739,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
     (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
      with Not_found ->
-       error_global_not_found ~loc (qualid_of_ident id))
+       error_global_not_found ?loc (qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
   | Inr c -> Inr (interp_typed_pattern ist env sigma c) in
   interp_occurrences ist occs, p
@@ -797,7 +797,7 @@ let interp_may_eval f ist env sigma = function
 	!evdref , c
       with
 	| Not_found ->
-	    user_err ~loc ~hdr:"interp_may_eval"
+	    user_err ?loc ~hdr:"interp_may_eval"
 	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
@@ -939,7 +939,7 @@ and interp_or_and_intro_pattern ist env sigma = function
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [loc,IntroNaming (IntroIdentifier id)] as l ->
-      (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun)
+      (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
          List.fold_map (interp_intro_pattern ist env) sigma l)
   | l -> List.fold_map (interp_intro_pattern ist env) sigma l
@@ -954,7 +954,7 @@ let interp_or_and_intro_pattern_option ist env sigma = function
       (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
-        user_err ~loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
+        user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
   | Some (ArgArg (loc,l)) ->
       let sigma,l = interp_or_and_intro_pattern ist env sigma l in
       sigma, Some (loc,l)
@@ -1011,13 +1011,13 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
 
 let loc_of_bindings = function
 | NoBindings         -> None
-| ImplicitBindings l -> Some (loc_of_glob_constr (fst (List.last l)))
-| ExplicitBindings l -> Some (fst (List.last l))
+| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
+| ExplicitBindings l -> fst (List.last l)
 
 let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
   let loc2 = loc_of_bindings bl in
-  let loc  = Loc.opt_merge loc1 loc2 in
+  let loc  = Loc.merge_opt loc1 loc2 in
   let f = { delayed = fun env sigma ->
     let sigma = Sigma.to_evar_map sigma in
     let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in
@@ -1035,7 +1035,7 @@ let interp_destruction_arg ist gl arg =
       }
   | keep,ElimOnAnonHyp n as x -> x
   | keep,ElimOnIdent (loc,id) ->
-      let error () = user_err ~loc 
+      let error () = user_err ?loc 
        (strbrk "Cannot coerce " ++ pr_id id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
@@ -1046,7 +1046,7 @@ let interp_destruction_arg ist gl arg =
           (keep, ElimOnConstr { delayed = begin fun env sigma ->
           try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
-            user_err ~loc  ~hdr:"interp_destruction_arg" (
+            user_err ?loc  ~hdr:"interp_destruction_arg" (
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
           end })
       in
@@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (Loc.tag ~loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
+          let c = (Loc.tag ?loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
@@ -1287,7 +1287,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
   | TacML (loc,(opn,l)) ->
-      push_trace (Loc.tag ~loc @@ LtacMLCall tac) ist >>= fun trace ->
+      push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace ->
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       let tac = Tacenv.interp_ml_tactic opn in
       let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 0ee6e8a859..4390ff08b4 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -242,7 +242,7 @@ and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
   | TacCall (loc,(f,l)) ->
-      TacCall (Loc.tag ~loc (subst_reference subst f, List.map (subst_tacarg subst) l))
+      TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l))
   | TacFreshId _ as x -> x
   | TacPretype c -> TacPretype (subst_glob_constr subst c)
   | TacNumgoals -> TacNumgoals
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index ac8534bdc4..f04495c61d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -387,12 +387,11 @@ let skip_extensions trace =
   | [] -> [] in
   List.rev (aux (List.rev trace))
 
-let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2
+let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2
 
 let extract_ltac_trace ?loc trace =
   let trace = skip_extensions trace in
   let (tloc,c),tail = List.sep_last trace in
-  let loc = Option.default tloc loc       in
   if is_defined_ltac trace then
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
@@ -405,8 +404,8 @@ let extract_ltac_trace ?loc trace =
       (* trace is with innermost call coming first *)
       let rec aux best_loc = function
         | (loc,_)::tail ->
-           if Loc.is_ghost best_loc ||
-              not (Loc.is_ghost loc) && finer_loc loc best_loc
+           if Option.is_empty best_loc ||
+              not (Option.is_empty loc) && finer_loc loc best_loc
            then
              aux loc tail
            else
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index a6a6bd6f98..0bc3f502ca 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -63,7 +63,7 @@ DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
-let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
+let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg)
 let ppnl = Feedback.msg_info
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
@@ -1071,7 +1071,7 @@ GEXTEND Gram
   GLOBAL: cpattern;
   cpattern: [[ k = ssrtermkind; c = constr ->
     let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
 END
 
 ARGUMENT EXTEND lcpattern
@@ -1088,7 +1088,7 @@ GEXTEND Gram
   GLOBAL: lcpattern;
   lcpattern: [[ k = ssrtermkind; c = lconstr ->
     let pattern = mk_term k c in
-    if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]];
+    if loc_ofCG pattern <> Some !@loc && k = '(' then mk_term 'x' c else pattern ]];
 END
 
 let thin id sigma goal =
@@ -1187,16 +1187,16 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red));
   let red = match redty with None -> red | Some ty -> let ty = ' ', ty in
   match red with
-  | T t -> T (combineCG t ty (mkCCast ~loc:(loc_ofCG t)) mkRCast)
+  | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast)
   | X_In_T (x,t) ->
       let ty = pf_intern_term ist gl ty in
       E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t)
   | E_In_X_In_T (e,x,t) ->
       let ty = mkG (pf_intern_term ist gl ty) in
-      E_In_X_In_T (combineCG e ty (mkCCast ~loc:(loc_ofCG t)) mkRCast, x, t)
+      E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | E_As_X_In_T (e,x,t) ->
       let ty = mkG (pf_intern_term ist gl ty) in
-      E_As_X_In_T (combineCG e ty (mkCCast ~loc:(loc_ofCG t)) mkRCast, x, t)
+      E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t)
   | red -> red in
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 894cdb9438..a8862d2646 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -222,7 +222,7 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
-val loc_of_cpattern : cpattern -> Loc.t
+val loc_of_cpattern : cpattern -> Loc.t option
 val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern