diff options
| author | Pierre-Marie Pédrot | 2017-08-07 16:39:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-07 16:42:16 +0200 |
| commit | 5062231251d58cf51cedb18677392b6e6d168694 (patch) | |
| tree | ab40cedc0b8c56e2abc29eb4a0de2fab38d2ac57 | |
| parent | bdd7bbb7875e596f802296a7a6ce0e77fd72fa51 (diff) | |
Defining several aliases for built-in tactics.
| -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 []. |