From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- grammar/argextend.mlp | 2 +- grammar/tacextend.mlp | 6 ++---- 2 files changed, 3 insertions(+), 5 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index d00ee4e5d..5ec8086d0 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -9,7 +9,7 @@ open Q_util let loc = Ploc.dummy -let default_loc = <:expr< Loc.ghost >> +let default_loc = <:expr< Loc.internal_ghost >> IFDEF STRICT THEN let ploc_vala x = Ploc.VaVal x diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 1dd8da12a..aa463ada5 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -20,8 +20,6 @@ let make_fun loc cl = let l = cl @ [default_patt loc] in MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) -let dloc = <:expr< Loc.ghost >> - let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = @@ -75,7 +73,7 @@ let rec mlexpr_of_symbol = function let make_prod_item = function | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >> + <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_ident id$ ) ) >> let mlexpr_of_clause cl = mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl @@ -114,7 +112,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with (** Arguments are not passed directly to the ML tactic in the TacML node, the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML ($dloc$, $ml$, [])) >> in + let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in let name = <:expr< Names.Id.of_string $name$ >> in declare_str_items loc [ <:str_item< do { -- cgit v1.2.3