diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.mlp | 1 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 4 |
2 files changed, 2 insertions, 3 deletions
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 |