diff options
| author | Pierre-Marie Pédrot | 2017-08-02 13:25:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-02 13:25:12 +0200 |
| commit | ebee89f2b2d1815dbb89916363de1b1ad17890e8 (patch) | |
| tree | eca2cecc33ce8d3d541261abf7feff1b10936460 | |
| parent | d0766f4dc08b00128a47a00ca74334ba0bfeed24 (diff) | |
Fixing parsing of match branches.
| -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 |