diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/tacentries.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index aedcb76eb7..714bfa8417 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -184,7 +184,6 @@ let add_tactic_entry (kn, ml, tg) state = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - synchronize_level_positions (); grammar_extend entry None (pos, [(None, None, List.rev [rules])]); (1, state) |