diff options
| -rw-r--r-- | test-suite/success/destruct.v | 4 | ||||
| -rw-r--r-- | test-suite/success/induct.v | 1 |
2 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index fb2c84c95..7adcc8de3 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -64,8 +64,8 @@ Abort. (* The calls to "destruct" below did not work before revision 12356 *) -Variable A:Type. -Variable P:A->Type. +Variable A0:Type. +Variable P:A0->Type. Require Import JMeq. Goal forall a b (p:P a) (q:P b), forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q). diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index aae55ec7a..8e1a8d183 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -39,4 +39,5 @@ Lemma foo : forall n m : nat, n + m = n + m. Proof. intros; induction m as [|m] in n |- *. auto. + auto. Qed. |