From 68e803063818235acdc6ade35767ee618f88fe89 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 16:27:44 +0200
Subject: The absurd tactic now parses a constr.

---
 theories/Notations.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Notations.v b/theories/Notations.v
index 9ecca018af..743210ae8d 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -435,7 +435,7 @@ Ltac2 Notation refine := Control.refine.
 
 Ltac2 absurd0 c := Control.enter (fun _ => Std.absurd (c ())).
 
-Ltac2 Notation absurd := absurd0.
+Ltac2 Notation "absurd" c(thunk(open_constr)) := absurd0 c.
 
 Ltac2 subst0 ids := match ids with
 | [] => Std.subst_all ()
-- 
cgit v1.2.3