diff options
Diffstat (limited to 'plugins/ltac/tacentries.ml')
| -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 |