diff options
| author | Pierre-Marie Pédrot | 2017-08-27 20:44:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-27 20:44:53 +0200 |
| commit | 0a5097752646f5bf3fd542880d4e33ece771f588 (patch) | |
| tree | 0bcc2b88394731fc245e40586beebf4aa88bccf7 | |
| parent | e430e9823960a136ee65c5977d89113574413449 (diff) | |
Notation for clear.
| -rw-r--r-- | theories/Notations.v | 8 |
1 files changed, 7 insertions, 1 deletions
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. |