From 947d93a8b7ff0fc7ba23633fcd44820427e29326 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 22 Mar 2017 19:31:18 +0100
Subject: Better compatibility of TACTIC EXTEND AT LEVEL with versions of
 camlp5.

This adds at least support for camlp5 6.14 (in addition to 6.17).
---
 grammar/tacextend.mlp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index 33ca2c629..8c0614a7b 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -135,7 +135,7 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
-        level = OPT [ "AT"; "LEVEL"; level = INT -> level ];
+        level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
         c = OPT [ "CLASSIFIED"; "BY"; c = LIDENT -> <:expr< $lid:c$ >> ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
-- 
cgit v1.2.3