From 3fbba861d5355cad92cac52965c8e76a35825c7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Aug 2017 14:21:11 +0200
Subject: Another batch of primitive operations.

---
 src/g_ltac2.ml4 | 8 ++++----
 src/tac2core.ml | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'src')

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)
-- 
cgit v1.2.3