diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 09:56:25 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 09:57:11 +0100 |
| commit | bcff4e5db054caec56acabc9d92ba36a8fc2eff6 (patch) | |
| tree | e5815297340fcbfee783ef056fd25311c270b04b /test-suite | |
| parent | a9adcb3941900c416f106ddac6fd646603b335b8 (diff) | |
Fixing clash in test destruct.v.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index a3b4b192e..26dab73ef 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -203,13 +203,13 @@ Qed. Abort. (* Test selection when not in an inductive type *) -Parameter A:Type. -Axiom elim: forall P, A -> P. -Goal forall a:A, a = a. +Parameter T:Type. +Axiom elim: forall P, T -> P. +Goal forall a:T, a = a. induction a using elim. Qed. -Goal forall a:nat -> A, a 0 = a 1. +Goal forall a:nat -> T, a 0 = a 1. intro a. induction (a 0) using elim. Qed. @@ -217,12 +217,12 @@ Qed. (* From Oct 2014, a subterm is found, as if without "using"; in 8.4, it did not find a subterm *) -Goal forall a:nat -> A, a 0 = a 1. +Goal forall a:nat -> T, a 0 = a 1. intro a. induction a using elim. Qed. -Goal forall a:nat -> A, forall b, a 0 = b. +Goal forall a:nat -> T, forall b, a 0 = b. intros a b. induction a using elim. Qed. |