diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-08 19:40:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:29:10 +0200 |
| commit | 9122623f2377bfe6aad0d4ea662481992e768201 (patch) | |
| tree | 3e16f7b6e1ba70c5dbae2e409586781f786d40d3 /grammar | |
| parent | e8a6467545c2814c9418889201e8be19c0cef201 (diff) | |
[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.
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 |