| Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical *
('term, 'lazy_term, 'reduction, 'ident) tactical list
| First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
+ (* try a sequence of loc * tactical until one succeeds, fail otherwise *)
| Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
(* try a tactical and mask failures *)
| Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
+ | Dot of loc
+ | Semicolon of loc
+ | Branch of loc
+ | Shift of loc
+ | Pos of loc * int
+ | Merge of loc
+ | Focus of loc * int list
+ | Unfocus of loc
+ | Skip of loc
+
+let is_punctuation =
+ function
+ | Dot _ | Semicolon _ | Branch _ | Shift _ | Merge _ | Pos _ -> true
+ | _ -> false
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
| Command of loc * ('term,'obj) command
| Macro of loc * 'term macro
| Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
+ * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
| Note of loc * string