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

4 files changed, 18 insertions, 18 deletions

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