From 0bfa6d3cda461f4d09ec0bfa9781042199b1f43b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 19 May 2017 15:25:58 +0200
Subject: Adding new tactic notation scopes.

---
 tac2core.ml | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/tac2core.ml b/tac2core.ml
index 94758eb217..c82893efc2 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -577,6 +577,27 @@ let () = add_scope "list0" begin function
 | _ -> scope_fail ()
 end
 
+let () = add_scope "list1" begin function
+| [tok] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let scope = Extend.Alist1 scope in
+  let act l =
+    let l = List.map act l in
+    CTacLst (Loc.ghost, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| [tok; SexprStr (_, str)] ->
+  let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
+  let sep = Extend.Atoken (CLexer.terminal str) in
+  let scope = Extend.Alist1sep (scope, sep) in
+  let act l =
+    let l = List.map act l in
+    CTacLst (Loc.ghost, l)
+  in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_scope "opt" begin function
 | [tok] ->
   let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in
@@ -599,5 +620,27 @@ let () = add_scope "self" begin function
 | _ -> scope_fail ()
 end
 
+let () = add_scope "next" begin function
+| [] ->
+  let scope = Extend.Anext in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
+let () = add_scope "tactic" begin function
+| [] ->
+  (** Default to level 5 parsing *)
+  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| [SexprInt (loc, n)] ->
+  let () = if n < 0 || n > 5 then scope_fail () in
+  let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
+  let act tac = rthunk tac in
+  Tac2entries.ScopeRule (scope, act)
+| _ -> scope_fail ()
+end
+
 let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
-- 
cgit v1.2.3