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. --- grammar/argextend.mlp | 1 - grammar/vernacextend.mlp | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) (limited to 'grammar') 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 -- cgit v1.2.3