From bcff4e5db054caec56acabc9d92ba36a8fc2eff6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Oct 2014 09:56:25 +0100
Subject: Fixing clash in test destruct.v.

---
 test-suite/success/destruct.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index a3b4b192ee..26dab73ef6 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.
-- 
cgit v1.2.3