[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.

6 files changed, 28 insertions, 28 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e58ec5a31f..ff8b54ebfb 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -86,7 +86,7 @@ let print_rewrite_hintdb bas =
 	       Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
-type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
+type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
@@ -291,12 +291,12 @@ let decompose_applied_relation metas env sigma c ctype left2right =
 	| Some c -> Some c
 	| None -> None
 
-let find_applied_relation metas loc env sigma c left2right =
+let find_applied_relation ?loc metas env sigma c left2right =
   let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
-	user_err ~loc ~hdr:"decompose_applied_relation"
+	user_err ?loc ~hdr:"decompose_applied_relation"
 		    (str"The type" ++ spc () ++ Printer.pr_econstr_env env sigma ctype ++
 		       spc () ++ str"of this term does not end with an applied relation.")
 
@@ -309,9 +309,9 @@ let add_rew_rules base lrul =
   let intern tac = snd (Genintern.generic_intern ist tac) in
   let lrul =
     List.fold_left
-      (fun dn (loc,(c,ctx),b,t) ->
+      (fun dn (loc,((c,ctx),b,t)) ->
 	let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
-	let info = find_applied_relation false loc env sigma c b in
+	let info = find_applied_relation ?loc false env sigma c b in
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_ctx = ctx; rew_l2r = b;
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 49e8588da3..f765318d04 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -12,7 +12,7 @@ open Term
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
-type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
+type raw_rew_rule = (constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option) Loc.located
 
 (** To add rewriting rules to a base *)
 val add_rew_rules : string -> raw_rew_rule list -> unit
@@ -56,7 +56,7 @@ type hypinfo = {
   hyp_right : constr;
 }
 
-val find_applied_relation : bool ->
-  Loc.t ->
+val find_applied_relation :
+  ?loc:Loc.t -> bool ->
   Environ.env -> Evd.evar_map -> Term.constr -> bool -> hypinfo
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index bcc068d3da..52e3dd09fe 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1282,7 +1282,7 @@ let interp_hints poly =
       prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
-    Dumpglob.add_glob (loc_of_reference r) gr;
+    Dumpglob.add_glob ?loc:(loc_of_reference r) gr;
     gr in
   let fr r = 
     evaluable_of_global_reference (Global.env()) (fref r)
@@ -1311,7 +1311,7 @@ let interp_hints poly =
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
 	let mib,_ = Global.lookup_inductive ind in
-	Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
+	Dumpglob.dump_reference ?loc:(fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
           List.init (nconstructors ind) 
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f2147db40a..a50ac31e1d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -283,9 +283,9 @@ let generalizeRewriteIntros as_mode tac depids id =
   end }
 
 let error_too_many_names pats =
-  let loc = Loc.merge (fst (List.hd pats)) (fst (List.last pats)) in
+  let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
   Proofview.tclENV >>= fun env ->
-  tclZEROMSG ~loc (
+  tclZEROMSG ?loc (
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
     str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed env Evd.empty c))))) pats ++
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 074c8b9de8..5c89331b88 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -187,7 +187,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
   | IntroAndPattern l ->
       if not (Int.equal n 1) then errn n;
       let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in
-      if l' != [] then errforthcoming ~loc:(fst (List.hd l'));
+      if l' != [] then errforthcoming ?loc:(fst (List.hd l'));
       if check_and then
         let p1 = List.count (fun x -> x) branchsigns.(0) in
         let p2 = List.length branchsigns.(0) in
@@ -221,7 +221,7 @@ let compute_induction_names_gen check_and branchletsigns = function
       Array.make (Array.length branchletsigns) []
   | Some (loc,names) ->
       let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
-      get_and_check_or_and_pattern_gen check_and ~loc names branchletsigns
+      get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns
 
 let compute_induction_names = compute_induction_names_gen true
 
@@ -492,7 +492,7 @@ module New = struct
     | [] -> ()
     | (evk,evi) :: _ ->
       let (loc,_) = evi.Evd.evar_source in
-      Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None
+      Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None
 
   let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7dad90242c..d265269b8a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -443,7 +443,7 @@ let find_name mayrepl decl naming gl = match naming with
       let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
       let id' = next_ident_away id ids_of_hyps in
       if not mayrepl && not (Id.equal id' id) then
-        user_err ~loc  (pr_id id ++ str" is already used.");
+        user_err ?loc  (pr_id id ++ str" is already used.");
       id
 
 (**************************************************************)
@@ -1734,7 +1734,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
       with Redelimination ->
         (* Last chance: if the head is a variable, apply may try
             second order unification *)
-        let info = Loc.add_loc info loc in
+        let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
         let tac =
           if with_destruct then
             descend_in_conjunctions []
@@ -1838,8 +1838,8 @@ let progress_with_clause flags innerclause clause =
   try List.find_map f ordered_metas
   with Not_found -> raise UnableToApply
 
-let explain_unable_to_apply_lemma loc env sigma thm innerclause =
-  user_err ~loc (hov 0
+let explain_unable_to_apply_lemma ?loc env sigma thm innerclause =
+  user_err ?loc (hov 0
     (Pp.str "Unable to apply lemma of type" ++ brk(1,1) ++
      Pp.quote (Printer.pr_leconstr_env env sigma thm) ++ spc() ++
      str "on hypothesis of type" ++ brk(1,1) ++
@@ -1855,7 +1855,7 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
     try aux (clenv_push_prod clause)
     with NotExtensibleClause ->
       match e with
-      | UnableToApply -> explain_unable_to_apply_lemma loc env sigma thm innerclause
+      | UnableToApply -> explain_unable_to_apply_lemma ?loc env sigma thm innerclause
       | _ -> iraise e'
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
@@ -2281,7 +2281,7 @@ let error_unexpected_extra_pattern loc bound pat =
   | IntroNaming (IntroIdentifier _) ->
       "name", (String.plural nb " introduction pattern"), "no"
   | _ -> "introduction pattern", "", "none" in
-  user_err ~loc  (str "Unexpected " ++ str s1 ++ str " (" ++
+  user_err ?loc  (str "Unexpected " ++ str s1 ++ str " (" ++
     (if Int.equal nb 0 then (str s3 ++ str s2) else
       (str "at most " ++ int nb ++ str s2)) ++ spc () ++
        str (if Int.equal nb 1 then "was" else "were") ++
@@ -2461,7 +2461,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
 	destopt true false
-        (intro_pattern_action ~loc with_evars (b || not (List.is_empty l)) false
+        (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false
           pat thin destopt
           (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
             (fun ids thin ->
@@ -2498,9 +2498,9 @@ and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
       rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
   | IntroApplyOn ((loc',f),(loc,pat)) ->
       let naming,tac_ipat =
-        prepare_intros ~loc with_evars (IntroIdentifier id) destopt pat in
+        prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in
       let doclear =
-        if naming = NamingMustBe (Loc.tag ~loc id) then
+        if naming = NamingMustBe (Loc.tag ?loc id) then
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
           clear [id] in
@@ -2549,7 +2549,7 @@ let intros_patterns with_evars = function
 
 let prepare_intros_opt with_evars dft destopt = function
   | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros ~loc with_evars dft destopt ipat
+  | Some (loc,ipat) -> prepare_intros ?loc with_evars dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
@@ -2692,7 +2692,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
       | IntroIdentifier id ->
           if List.mem id (ids_of_named_context (named_context env)) then
-            user_err ~loc  (pr_id id ++ str" is already used.");
+            user_err ?loc  (pr_id id ++ str" is already used.");
           id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -2973,7 +2973,7 @@ let specialize (c,lbind) ipat =
       | Some (loc,ipat) ->
         (* Like pose proof with extra support for "with" bindings *)
         (* even though the "with" bindings forces full application *)
-        let naming,tac = prepare_intros ~loc false IntroAnonymous MoveLast ipat in
+        let naming,tac = prepare_intros ?loc false IntroAnonymous MoveLast ipat in
         Tacticals.New.tclTHENFIRST
           (assert_before_then_gen false naming typ tac)
 	  (exact_no_check term)
@@ -4467,7 +4467,7 @@ let induction_gen_l isrec with_evars elim names lc =
   let lc = List.map (function
     | (c,None) -> c
     | (c,Some(loc,eqname)) ->
-      user_err ~loc  (str "Do not know what to do with " ++
+      user_err ?loc  (str "Do not know what to do with " ++
                          Miscprint.pr_intro_pattern_naming eqname)) lc in
   let rec atomize_list l =
     match l with