[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, 62 insertions, 58 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index c8fe96f74..49bf267db 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -313,13 +313,13 @@ let interp_entry forpat e = match e with
 | ETBinderList (true, _) -> assert false
 | ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl)
 
-let constr_expr_of_name (loc,na) = Loc.tag ~loc @@ match na with
+let constr_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
   | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None)
-  | Name id   -> CRef (Ident (loc,id), None)
+  | Name id   -> CRef (Ident (Loc.tag ?loc id), None)
 
-let cases_pattern_expr_of_name (loc,na) = Loc.tag ~loc @@ match na with
+let cases_pattern_expr_of_name (loc,na) = Loc.tag ?loc @@ match na with
   | Anonymous -> CPatAtom None
-  | Name id   -> CPatAtom (Some (Ident (loc,id)))
+  | Name id   -> CPatAtom (Some (Ident (Loc.tag ?loc id)))
 
 type 'r env = {
   constrs : 'r list;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e6c82c894..45585d9ce 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -33,12 +33,12 @@ let _ = List.iter CLexer.add_keyword constr_kw
 let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
-    let loc = Loc.merge (constr_loc c) (constr_loc ty)
-    in Loc.tag ~loc @@ CCast(c, CastConv ty)
+    let loc = Loc.merge_opt (constr_loc c) (constr_loc ty)
+    in Loc.tag ?loc @@ CCast(c, CastConv ty)
 
 let binder_of_name expl (loc,na) =
   CLocalAssum ([loc, na], Default expl,
-    Loc.tag ~loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
+    Loc.tag ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None))
 
 let binders_of_names l =
   List.map (binder_of_name Explicit) l
@@ -51,7 +51,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
-    CErrors.user_err ~loc:aloc
+    CErrors.user_err ?loc:aloc
       ~hdr:"Constr:mk_cofixb"
       (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
@@ -131,7 +131,7 @@ GEXTEND Gram
     [ [ id = Prim.ident -> id ] ]
   ;
   Prim.name:
-    [ [ "_" -> (!@loc, Anonymous) ] ]
+    [ [ "_" -> Loc.tag ~loc:!@loc Anonymous ] ]
   ;
   global:
     [ [ r = Prim.reference -> r ] ]
@@ -183,13 +183,13 @@ GEXTEND Gram
     | "90" RIGHTA [ ]
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> Loc.tag ~loc:(!@loc) @@ CApp((None,f),args)
-      | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:(!@loc) @@ CAppExpl((None,f,i),args)
+      | "@"; f=global; i = instance; args=LIST0 NEXT -> Loc.tag ~loc:!@loc @@ CAppExpl((None,f,i),args)
       | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
           let args = List.map (fun x -> Loc.tag @@ CRef (Ident x,None), None) args in
-          Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ~loc:locid @@ CPatVar id),args) ]
+          Loc.tag ~loc:(!@loc) @@ CApp((None, Loc.tag ?loc:locid @@ CPatVar id),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
-          Loc.tag ~loc:(!@loc) @@ CAppExpl ((None, Ident (!@loc,ldots_var),None),[c]) ]
+          Loc.tag ~loc:!@loc @@ CAppExpl ((None, Ident (Loc.tag ~loc:!@loc ldots_var),None),[c]) ]
     | "8" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
@@ -236,10 +236,10 @@ GEXTEND Gram
       | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           let ty,c1 = match ty, c1 with
-          | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ~loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
+          | (_,None), (_, CCast(c, CastConv t)) -> (Loc.tag ?loc:(constr_loc t) @@ Some t), c (* Tolerance, see G_vernac.def_body *)
           | _, _ -> ty, c1 in
-          Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ~loc:(constr_loc c1) bl c1,
-                 Option.map (mkCProdN ~loc:(fst ty) bl) (snd ty), c2)
+          Loc.tag ~loc:!@loc @@ CLetIn(id,mkCLambdaN ?loc:(constr_loc c1) bl c1,
+                 Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
           let (li,id) = match snd fixp with
@@ -254,14 +254,18 @@ GEXTEND Gram
           Loc.tag ~loc:!@loc @@ CLetTuple (lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+	    Loc.tag ~loc:!@loc @@
+            CCases (LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+	    Loc.tag ~loc:!@loc @@
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
+
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    Loc.tag ~loc:!@loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
+	    Loc.tag ~loc:!@loc @@
+            CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -270,7 +274,7 @@ GEXTEND Gram
   ;
   appl_arg:
     [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
-	  (c,Some (!@loc,ExplByName id))
+	  (c,Some (Loc.tag ~loc:!@loc @@ ExplByName id))
       | c=operconstr LEVEL "9" -> (c,None) ] ]
   ;
   atomic_constr:
@@ -345,7 +349,7 @@ GEXTEND Gram
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
   ;
   mult_pattern:
-    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (!@loc,pl) ] ]
+    [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ]
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
@@ -364,7 +368,7 @@ GEXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> !@loc, CPatOr (p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> Loc.tag ~loc:!@loc @@ CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
@@ -374,21 +378,21 @@ GEXTEND Gram
         (match p with
 	  | _,   CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
 	  | loc, CPatCstr (r, None, l2) ->
-                 CErrors.user_err ~loc ~hdr:"compound_pattern"
+                 CErrors.user_err ?loc ~hdr:"compound_pattern"
                  (Pp.str "Nested applications not supported.")
 	  | _,   CPatCstr (r, l1, l2)   -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
 	  | _,   CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp)
           | _ -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
-              (Pp.str "Such pattern cannot have arguments."))
+                 ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
+                 (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
-        !@loc, CPatCstr (r, Some lp, []) ]
+        Loc.tag ~loc:!@loc @@ CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> !@loc, CPatDelimiters (key,c) ]
+      [ c = pattern; "%"; key=IDENT -> Loc.tag ~loc:!@loc @@ CPatDelimiters (key,c) ]
     | "0"
       [ r = Prim.reference                -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
       | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
-      | "_" -> !@loc, CPatAtom None
+      | "_" -> Loc.tag ~loc:!@loc @@ CPatAtom None
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
             | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
@@ -401,7 +405,7 @@ GEXTEND Gram
                  Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
-	  !@loc, CPatCast (p, ty)
+	  Loc.tag ~loc:!@loc @@ CPatCast (p, ty)
       | n = INT    -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
       | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
@@ -411,7 +415,7 @@ GEXTEND Gram
         (fun na -> CLocalAssum (na::nal,Default Implicit,c))
     | nal=LIST1 name; "}" ->
         (fun na -> CLocalAssum (na::nal,Default Implicit,
-                                Loc.tag ~loc:(Loc.merge (fst na) !@loc) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+                                Loc.tag ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
     | ":"; c=lconstr; "}" ->
 	(fun na -> CLocalAssum ([na],Default Implicit,c))
     ] ]
@@ -424,7 +428,7 @@ GEXTEND Gram
     ] ]
   ;
   impl_name_head:
-    [ [ id = impl_ident_head -> (!@loc,Name id) ] ]
+    [ [ id = impl_ident_head -> (Loc.tag ~loc:!@loc @@ Name id) ] ]
   ;
   binders_fixannot:
     [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
@@ -444,7 +448,7 @@ GEXTEND Gram
       | id = name; idl = LIST0 name; bl = binders ->
           binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
-          [CLocalAssum ([id1;(!@loc,Name ldots_var);id2],
+          [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2],
 	                  Default Explicit, Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, None))]
       | bl = closed_binder; bl' = binders ->
 	  bl@bl'
@@ -490,17 +494,17 @@ GEXTEND Gram
     ] ]
   ;
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (!@loc, Anonymous), true, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (Loc.tag ~loc:!@loc Anonymous), true, c
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
       | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
-	  (!@loc, iid), expl, c
+	  (Loc.tag ~loc:!@loc iid), expl, c
       | c = operconstr LEVEL "200" ->
-	  (!@loc, Anonymous), false, c
+	  (Loc.tag ~loc:!@loc Anonymous), false, c
     ] ]
   ;
 
   type_cstr:
-    [ [ c=OPT [":"; c=lconstr -> c] -> (!@loc,c) ] ]
+    [ [ c=OPT [":"; c=lconstr -> c] -> Loc.tag ~loc:!@loc c ] ]
   ;
   END;;
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index ed6a8df4e..d94c5e963 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -44,13 +44,13 @@ GEXTEND Gram
     [ [ LEFTQMARK; id = ident -> id ] ]
   ;
   pattern_identref:
-    [ [ id = pattern_ident -> (!@loc, id) ] ]
+    [ [ id = pattern_ident -> Loc.tag ~loc:!@loc id ] ]
   ;
   var: (* as identref, but interpret as a term identifier in ltac *)
-    [ [ id = ident -> (!@loc, id) ] ]
+    [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
   ;
   identref:
-    [ [ id = ident -> (!@loc, id) ] ]
+    [ [ id = ident -> Loc.tag ~loc:!@loc id ] ]
   ;
   field:
     [ [ s = FIELD -> Id.of_string s ] ]
@@ -61,8 +61,8 @@ GEXTEND Gram
       ] ]
   ;
   fullyqualid:
-    [ [ id = ident; (l,id')=fields -> !@loc,id::List.rev (id'::l)
-      | id = ident -> !@loc,[id]
+    [ [ id = ident; (l,id')=fields -> Loc.tag ~loc:!@loc @@ id::List.rev (id'::l)
+      | id = ident -> Loc.tag ~loc:!@loc [id]
       ] ]
   ;
   basequalid:
@@ -71,13 +71,13 @@ GEXTEND Gram
       ] ]
   ;
   name:
-    [ [ IDENT "_" -> (!@loc, Anonymous)
-      | id = ident -> (!@loc, Name id) ] ]
+    [ [ IDENT "_"  -> Loc.tag ~loc:!@loc Anonymous
+      | id = ident -> Loc.tag ~loc:!@loc @@ Name id ] ]
   ;
   reference:
     [ [ id = ident; (l,id') = fields ->
-        Qualid (!@loc, local_make_qualid (l@[id]) id')
-      | id = ident -> Ident (!@loc,id)
+        Qualid (Loc.tag ~loc:!@loc @@ local_make_qualid (l@[id]) id')
+      | id = ident -> Ident (Loc.tag ~loc:!@loc id)
       ] ]
   ;
   by_notation:
@@ -88,15 +88,15 @@ GEXTEND Gram
       | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
   ;
   qualid:
-    [ [ qid = basequalid -> !@loc, qid ] ]
+    [ [ qid = basequalid -> Loc.tag ~loc:!@loc qid ] ]
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
+        if s="" then CErrors.user_err ~loc:!@loc (Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
-    [ [ s = ne_string -> (!@loc, s) ] ]
+    [ [ s = ne_string -> Loc.tag ~loc:!@loc s ] ]
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
@@ -106,7 +106,7 @@ GEXTEND Gram
     [ [ s = STRING -> s ] ]
   ;
   lstring:
-    [ [ s = string -> (!@loc, s) ] ]
+    [ [ s = string -> (Loc.tag ~loc:!@loc s) ] ]
   ;
   integer:
     [ [ i = INT      -> my_int_of_string (!@loc) i
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 7a3a2ace1..c8101875d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -102,7 +102,7 @@ GEXTEND Gram
   ;
 
   located_vernac:
-    [ [ v = vernac -> !@loc, v ] ]
+    [ [ v = vernac -> Loc.tag ~loc:!@loc v ] ]
   ;
 END
 
@@ -542,8 +542,8 @@ GEXTEND Gram
   starredidentref:
     [ [ i = identref -> SsSingl i
       | i = identref; "*" -> SsFwdClose(SsSingl i)
-      | "Type" -> SsSingl (!@loc, Id.of_string "Type")
-      | "Type"; "*" -> SsFwdClose (SsSingl (!@loc, Id.of_string "Type")) ]]
+      | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")
+      | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]]
   ;
   ssexpr:
     [ "35" 
@@ -720,7 +720,7 @@ GEXTEND Gram
   ;
   argument_spec: [
        [ b = OPT "!"; id = name ; s = OPT scope ->
-       snd id, not (Option.is_empty b), Option.map (fun x -> !@loc, x) s
+       snd id, not (Option.is_empty b), Option.map (fun x -> Loc.tag ~loc:!@loc x) s
     ]
   ];
   (* List of arguments implicit status, scope, modifiers *)
@@ -733,7 +733,7 @@ GEXTEND Gram
     | "/" -> [`Slash]
     | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
        let f x = match sc, x with
-         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
          | Some _, Some _ -> error "scope declared twice" in
        List.map (fun (name,recarg_like,notation_scope) ->
            `Id { name=name; recarg_like=recarg_like;
@@ -741,7 +741,7 @@ GEXTEND Gram
                  implicit_status = NotImplicit}) items
     | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
        let f x = match sc, x with
-         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
          | Some _, Some _ -> error "scope declared twice" in
        List.map (fun (name,recarg_like,notation_scope) ->
            `Id { name=name; recarg_like=recarg_like;
@@ -749,7 +749,7 @@ GEXTEND Gram
                  implicit_status = Implicit}) items
     | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
        let f x = match sc, x with
-         | None, x -> x | x, None -> Option.map (fun y -> !@loc, y) x
+         | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x
          | Some _, Some _ -> error "scope declared twice" in
        List.map (fun (name,recarg_like,notation_scope) ->
            `Id { name=name; recarg_like=recarg_like;
@@ -782,7 +782,7 @@ GEXTEND Gram
     [ [ name = pidentref; sup = OPT binders ->
 	  (let ((loc,id),l) = name in ((loc, Name id),l)),
           (Option.default [] sup)
-      | -> ((!@loc, Anonymous), None), []  ] ]
+      | -> ((Loc.tag ~loc:!@loc Anonymous), None), []  ] ]
   ;
   hint_info:
     [ [ "|"; i = OPT natural; pat = OPT constr_pattern ->
@@ -1149,8 +1149,8 @@ GEXTEND Gram
       | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
       | IDENT "compat"; s = STRING ->
         SetCompatVersion (Coqinit.get_compat_version s)
-      | IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
-                        s2 = OPT [s = STRING -> (!@loc,s)] ->
+      | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s];
+                        s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] ->
           begin match s1, s2 with
           | (_,k), Some s -> SetFormat(k,s)
           | s, None -> SetFormat ("text",s) end