diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
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 |