[location] Remove `Loc.internal_ghost`

`internal_ghost` was an artifact to ease porting of the ml4 rules. Now
that the location is optional we can finally get rid of it.

8 files changed, 9 insertions, 19 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 96cb9443c..5fb0aebb5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -521,7 +521,7 @@ let _ =
   extend_vernac_command_grammar ("PrintConstr", 0) None
     [GramTerminal "PrintConstr";
       GramNonTerminal
-        (Loc.internal_ghost, rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 let _ =
   try
@@ -537,7 +537,7 @@ let _ =
   extend_vernac_command_grammar ("PrintPureConstr", 0) None
     [GramTerminal "PrintPureConstr";
       GramNonTerminal
-        (Loc.internal_ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+        (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 5ec8086d0..10ead2c29 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -9,7 +9,6 @@
 open Q_util
 
 let loc = Ploc.dummy
-let default_loc = <:expr< Loc.internal_ghost >>
 
 IFDEF STRICT THEN
   let ploc_vala x = Ploc.VaVal x
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 436a7f0d9..39155a014 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -104,8 +104,8 @@ let make_prod_item = function
   | ExtNonTerminal (g, id) ->
     let nt = type_of_user_symbol g in
     let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
-      $mlexpr_of_prod_entry_key base g$ >>
+      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $make_rawwit loc nt$ ,
+      $mlexpr_of_prod_entry_key base g$ ) ) >>
 
 let mlexpr_of_clause cl =
   let mkexpr { r_head = a; r_patt = b; } = match a with
diff --git a/lib/loc.ml b/lib/loc.ml
index e02fe108d..9107dce47 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -55,10 +55,6 @@ let unloc loc = (loc.bp, loc.ep)
 
 let join_loc = merge
 
-let internal_ghost = {
-  fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
-  bp = 0; ep = 0; }
-
 (** Located type *)
 type 'a located = t option * 'a
 
diff --git a/lib/loc.mli b/lib/loc.mli
index 6de6c584d..110920d5a 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -32,10 +32,6 @@ val unloc : t -> int * int
 val make_loc : int * int -> t
 (** Make a location out of its start and end position *)
 
-val internal_ghost : t
-
-(** Test whether the location is meaningful *)
-
 val merge : t -> t -> t
 val merge_opt : t option -> t option -> t option
 
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 97a3e89a5..1c6346a8f 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
 type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+      ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
 
 type 'a ty_arg = ('a -> raw_generic_argument)
 
@@ -36,7 +36,7 @@ let rec ty_rule_of_gram = function
   let tok = Atoken (CLexer.terminal s) in
   let r = TyNext (rem, tok, None) in
   AnyTyRule r
-| GramNonTerminal (_, t, tok) :: rem ->
+| GramNonTerminal (_, (t, tok)) :: rem ->
   let AnyTyRule rem = ty_rule_of_gram rem in
   let inj = Some (fun obj -> Genarg.in_gen t obj) in
   let r = TyNext (rem, tok, inj) in
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1ad947200..1a3ae173c 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,8 +15,8 @@ open Vernacexpr
 
 type 's grammar_prod_item =
   | GramTerminal of string
-  | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
-      ('s, 'a) Extend.symbol -> 's grammar_prod_item
+  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
+      ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
   Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a19dbd327..1de4024fd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -180,8 +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)
+    GramNonTerminal (Loc.tag ?loc (typ, e))
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in