type ('term, 'ident) tactic =
| Absurd of loc * 'term
| Apply of loc * 'term
- | Auto of loc
+ | Auto of loc * int option
| Assumption of loc
| Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
| Change_pattern of loc * 'term pattern * 'term * 'ident option
| Fold of loc * reduction_kind * 'term
| Fourier of loc
| Goal of loc * int (* change current goal, argument is goal number 1-based *)
- | Hint of loc
| Injection of loc * 'ident
| Intros of loc * int option * 'ident list
| Left of loc
type print_kind = [ `Env | `Coer ]
type 'term macro =
- | Abort of loc
+ (* Whelp's stuff *)
+ | WHint of loc * 'term
+ | WMatch of loc * 'term
+ | WInstance of loc * 'term
+ | WLocate of loc * string
+ | WElim of loc * 'term
+ (* real macros *)
+(* | Abort of loc *)
| Print of loc * string
| Check of loc * 'term
+ | Hint of loc
| Quit of loc
- | Redo of loc * int option
- | Undo of loc * int option
+(* | Redo of loc * int option
+ | Undo of loc * int option *)
(* | Print of loc * print_kind *)
| Search_pat of loc * search_kind * string (* searches with string pattern *)
| Search_term of loc * search_kind * 'term (* searches with term pattern *)
(* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
| Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
-type ('term, 'ident) statement =
+
+type ('term, 'ident) code =
| Command of loc * 'term command
| Macro of loc * 'term macro
(* Macro are substantially queries, but since we are not the kind of
* peolpe that like to push "start" to turn off the computer
* we added this command *)
| Tactical of loc * ('term, 'ident) tactical
+
+type ('term, 'ident) comment =
+ | Note of loc * string
+ | Code of loc * ('term, 'ident) code
+
+type ('term, 'ident) statement =
+ | Executable of loc * ('term, 'ident) code
+ | Comment of loc * ('term, 'ident) comment