diff options
| -rw-r--r-- | tests/example2.v | 4 | ||||
| -rw-r--r-- | theories/Notations.v | 12 |
2 files changed, 14 insertions, 2 deletions
diff --git a/tests/example2.v b/tests/example2.v index 76f069a5ae..bfb1b07e7a 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -5,7 +5,7 @@ Import Ltac2.Notations. Goal exists n, n = 0. Proof. split with (x := 0). -Std.reflexivity (). +reflexivity. Qed. Goal exists n, n = 0. @@ -113,7 +113,7 @@ Qed. Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0. Proof. intros n m He He' He''. -rewrite <- &He by Std.assumption (). +rewrite <- &He by assumption. Control.refine (fun () => &He''). Qed. diff --git a/theories/Notations.v b/theories/Notations.v index d7f7170a5e..0fa3456196 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -242,3 +242,15 @@ Ltac2 Notation "erewrite" cl(opt(clause)) tac(opt(seq("by", thunk(tactic)))) := rewrite0 true rw cl tac. + +(** Other base tactics *) + +Ltac2 Notation reflexivity := Std.reflexivity (). + +Ltac2 Notation assumption := Std.assumption (). + +Ltac2 Notation etransitivity := Std.etransitivity (). + +Ltac2 Notation admit := Std.admit (). + +Ltac2 Notation clear := Std.keep []. |