diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Rename.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index 8a5db157c0..0576f3c68f 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -3,3 +3,16 @@ intros. rename n into p. induction p; auto. Qed. + +(* Submitted by Iris Loeb (#842) *) + +Section rename. + +Variable A:Prop. + +Lemma Tauto: A->A. +rename A into B. +tauto. +Qed. + +End rename. |