diff options
| author | Pierre-Marie Pédrot | 2017-10-30 18:16:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 18:16:18 +0100 |
| commit | de7483beb78e5bd81dc6449ba201fb9dfc490ba8 (patch) | |
| tree | 607bccab68053410b42f4d767cf7a5dd6aae61f6 | |
| parent | 2f95db622428cf58968e8d13f2230fe51c31e97f (diff) | |
Add a macro for the now tactic
| -rw-r--r-- | theories/Notations.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 77f3e235f3..dc09812254 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -555,3 +555,8 @@ Ltac2 Notation "firstorder" tac(opt(thunk(tactic))) refs(opt(seq("using", list1(reference, ",")))) ids(opt(seq("with", list1(ident)))) := firstorder0 tac refs ids. + +(** now *) + +Ltac2 now0 t := t (); ltac1:(easy). +Ltac2 Notation "now" t(thunk(self)) := now0 t. |