From 85753a0bdb6183604a78232c4c32fd15f7a21a2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 11 May 2016 13:25:02 +0200
Subject: Moving the constr empty entry registering to the state-based API.

---
 ltac/tacentries.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'ltac')

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)
 
-- 
cgit v1.2.3