From de7483beb78e5bd81dc6449ba201fb9dfc490ba8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 30 Oct 2017 18:16:18 +0100
Subject: Add a macro for the now tactic

---
 theories/Notations.v | 5 +++++
 1 file changed, 5 insertions(+)

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