From c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 9 Apr 2016 16:39:07 +0200
Subject: Honor parsing and printing levels for tactic entry in TACTIC EXTEND
 and VERNAC EXTEND.

---
 grammar/q_util.ml4 | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index c529260e9..8a876de9b 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -79,7 +79,8 @@ let rec type_of_user_symbol = function
   ListArgType (type_of_user_symbol s)
 | Uopt s ->
   OptArgType (type_of_user_symbol s)
-| Uentry e | Uentryl (e, _) -> ExtraArgType e
+| Uentry e -> ExtraArgType e
+| Uentryl (e, n) -> ExtraArgType (e ^ string_of_int n)
 
 let coincide s pat off =
   let len = String.length pat in
-- 
cgit v1.2.3