From fb77937a6ba0fe45e978911db08de57f931683e1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Dec 2015 23:38:00 +0100
Subject: Changing syntax of pat/constr1.../constrn into
 pat%constr1...%constrn. Marking it as experimental.

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

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4d42dfe85a..3d59b9b8db 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -311,7 +311,8 @@ GEXTEND Gram
       | "**" -> !@loc, IntroForthcoming false ]]
   ;
   simple_intropattern:
-    [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] ->
+    [ [ pat = simple_intropattern_closed;
+        l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
           let loc0,pat = pat in
           let f c pat =
             let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
-- 
cgit v1.2.3