From 0a5097752646f5bf3fd542880d4e33ece771f588 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Aug 2017 20:44:53 +0200
Subject: Notation for clear.

---
 theories/Notations.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/Notations.v b/theories/Notations.v
index ea31d4ef47..46c0e5e79f 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -329,7 +329,13 @@ Ltac2 Notation etransitivity := Std.etransitivity ().
 
 Ltac2 Notation admit := Std.admit ().
 
-Ltac2 Notation clear := Std.keep [].
+Ltac2 clear0 ids := match ids with
+| [] => Std.keep []
+| _ => Std.clear ids
+end.
+
+Ltac2 Notation "clear" ids(list0(ident)) := clear0 ids.
+Ltac2 Notation clear := clear.
 
 Ltac2 Notation refine := Control.refine.
 
-- 
cgit v1.2.3