From ac3bb720d4ec04aa670845352df1d8b8885f865e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Sep 2017 22:42:33 +0200
Subject: Notation for "clear - ids".

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

diff --git a/theories/Notations.v b/theories/Notations.v
index ad89bc5cfc..136ca871c2 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -401,6 +401,7 @@ Ltac2 clear0 ids := match ids with
 end.
 
 Ltac2 Notation "clear" ids(list0(ident)) := clear0 ids.
+Ltac2 Notation "clear" "-" ids(list1(ident)) := Std.keep ids.
 Ltac2 Notation clear := clear.
 
 Ltac2 Notation refine := Control.refine.
-- 
cgit v1.2.3