diff options
| author | Pierre-Marie Pédrot | 2017-09-14 15:37:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-14 15:54:48 +0200 |
| commit | 6218f06931384a38445e9d829e6782c069c3ffb4 (patch) | |
| tree | 3aa360a0b0352fc915064c004a2e32d69f53c0df /tests | |
| parent | c53fb4be8c65a89dd03d4aedc2fc65d9807da915 (diff) | |
Introducing the remember tactic.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/example2.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tests/example2.v b/tests/example2.v index b667e19bbd..a21f3a7f4e 100644 --- a/tests/example2.v +++ b/tests/example2.v @@ -222,3 +222,9 @@ set ($x := True) in * |-. constructor. Qed. +Goal 0 = 0. +Proof. +remember 0 as n eqn: foo at 1. +rewrite foo. +reflexivity. +Qed. |