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 /tests | |
| parent | bdd7bbb7875e596f802296a7a6ce0e77fd72fa51 (diff) | |
Defining several aliases for built-in tactics.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 4 |
1 files changed, 2 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. |