diff options
| author | Pierre-Marie Pédrot | 2017-09-05 01:39:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:39:51 +0200 |
| commit | ca40f89c7be05253ea04585ac9ce068aa4744ae9 (patch) | |
| tree | f1308142e67cc74c2e06a7a15b526d393d310652 | |
| parent | 4a8399e62dd4bdf5876e714910dd2c7cb433dfda (diff) | |
A few more notations.
| -rw-r--r-- | theories/Notations.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 5fdb4ec8af..75abb2f1cd 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -389,6 +389,8 @@ Ltac2 symmetry0 cl := Ltac2 Notation "symmetry" cl(opt(clause)) := symmetry0 cl. Ltac2 Notation symmetry := symmetry. +Ltac2 Notation "revert" ids(list1(ident)) := Std.revert ids. + Ltac2 Notation assumption := Std.assumption (). Ltac2 Notation etransitivity := Std.etransitivity (). @@ -422,9 +424,11 @@ Ltac2 Notation subst := subst. Ltac2 Notation "discriminate" arg(opt(destruction_arg)) := Std.discriminate false arg. +Ltac2 Notation discriminate := discriminate. Ltac2 Notation "ediscriminate" arg(opt(destruction_arg)) := Std.discriminate true arg. +Ltac2 Notation ediscriminate := ediscriminate. Ltac2 Notation "injection" arg(opt(destruction_arg)) ipat(opt(seq("as", intropatterns))):= Std.injection false ipat arg. |