diff options
| author | Pierre-Marie Pédrot | 2017-08-08 14:21:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-08 15:26:11 +0200 |
| commit | 3fbba861d5355cad92cac52965c8e76a35825c7a (patch) | |
| tree | 4d90154704a17a98f822552711fe78c8fe24adb6 /src | |
| parent | 3d1092cf7df3229ecc2a4da60a33cf7c6b9be1a3 (diff) | |
Another batch of primitive operations.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 8 | ||||
| -rw-r--r-- | src/tac2core.ml | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 9bc7107cc7..695fc7d430 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -97,13 +97,13 @@ GEXTEND Gram ] ; tac2expr: - [ "top" RIGHTA + [ "6" RIGHTA [ e1 = SELF; ";"; e2 = SELF -> CTacSeq (!@loc, e1, e2) ] | "5" - [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "top" -> CTacFun (!@loc, it, body) + [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" -> CTacFun (!@loc, it, body) | "let"; isrec = rec_flag; lc = LIST1 let_clause SEP "with"; "in"; - e = tac2expr LEVEL "top" -> CTacLet (!@loc, isrec, lc, e) + e = tac2expr LEVEL "6" -> CTacLet (!@loc, isrec, lc, e) | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" -> CTacCse (!@loc, e, bl) ] @@ -135,7 +135,7 @@ GEXTEND Gram ] ; branch: - [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "top" -> (pat, e) ] ] + [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> (pat, e) ] ] ; rec_flag: [ [ IDENT "rec" -> true diff --git a/src/tac2core.ml b/src/tac2core.ml index 08f61f2c6c..1c03cc410d 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -877,7 +877,7 @@ let () = add_scope "tactic" begin function let act tac = tac in Tac2entries.ScopeRule (scope, act) | [SexprInt (loc, n)] -> - let () = if n < 0 || n > 5 then scope_fail () in + let () = if n < 0 || n > 6 then scope_fail () in let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in let act tac = tac in Tac2entries.ScopeRule (scope, act) |