diff options
Diffstat (limited to 'grammar')
-rw-r--r-- | grammar/argextend.mlp | 1 | ||||
-rw-r--r-- | grammar/tacextend.mlp | 6 | ||||
-rw-r--r-- | grammar/vernacextend.mlp | 4 |
3 files changed, 4 insertions, 7 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 5cfcc6fd2..c736e1a74 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.ghost >> IFDEF STRICT THEN let ploc_vala x = Ploc.VaVal x diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 3057ee58c..8e3dccf47 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_option mlexpr_of_ident id$ >> + <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option 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 { diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 7c99b52e8..4f9a7c75c 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -105,8 +105,8 @@ let make_prod_item = function let nt = type_of_user_symbol g in let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in let typ = match ido with None -> None | Some _ -> Some nt in - <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_option (make_rawwit loc) typ$ - $mlexpr_of_prod_entry_key base g$ >> + <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ , + $mlexpr_of_prod_entry_key base g$ ) ) >> let mlexpr_of_clause cl = let mkexpr { r_head = a; r_patt = b; } = match a with |