From 9122623f2377bfe6aad0d4ea662481992e768201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Apr 2017 19:40:57 +0200 Subject: [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. --- dev/top_printers.ml | 4 ++-- grammar/argextend.mlp | 1 - grammar/vernacextend.mlp | 4 ++-- lib/loc.ml | 4 ---- lib/loc.mli | 4 ---- parsing/egramml.ml | 4 ++-- parsing/egramml.mli | 4 ++-- plugins/ltac/tacentries.ml | 3 +-- 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 -- cgit v1.2.3