From ebee89f2b2d1815dbb89916363de1b1ad17890e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Aug 2017 13:25:12 +0200
Subject: Fixing parsing of match branches.

---
 src/g_ltac2.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 3c41828cd3..20a00afa2e 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -90,7 +90,7 @@ GEXTEND Gram
       | "let"; isrec = rec_flag;
           lc = LIST1 let_clause SEP "with"; "in";
           e = tac2expr LEVEL "top" -> CTacLet (!@loc, isrec, lc, e)
-      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches ;"end" ->
+      | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
          CTacCse (!@loc, e, bl)
       ]
     | "::" RIGHTA
@@ -121,7 +121,7 @@ GEXTEND Gram
   ]
   ;
   branch:
-  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "5" -> (pat, e) ] ]
+  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "top" -> (pat, e) ] ]
   ;
   rec_flag:
     [ [ IDENT "rec" -> true
-- 
cgit v1.2.3