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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a19dbd327..1de4024fd 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -180,8 +180,7 @@ let add_tactic_entry (kn, ml, tg) state = | TacTerm s -> GramTerminal s | TacNonTerm (loc, (s, _)) -> let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - let loc = Option.default Loc.internal_ghost loc in - GramNonTerminal (loc, typ, e) + GramNonTerminal (Loc.tag ?loc (typ, e)) in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in |