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

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 074c8b9de..5c89331b8 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 ->