From 4c3301517cf8887b3684fda58e2e4626a072a5fb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 15 May 2008 12:51:59 +0000
Subject: Various fixes: - Fix a typo in lowercase_utf8 - Fix generation of
 signatures in subtac_cases not working for dependent inductive types with
 dependent indices. - Fix coercion of inductive types generating ill-typed
 terms. - Fix test script using new syntax for Instances. - Move simpl_existTs
 to Program.Equality and use it in simpl_depind.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/dependentind.v | 8 ++++----
 test-suite/success/setoid_test2.v | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index be7b77ef00..0db172e82a 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -17,9 +17,9 @@ Require Import ProofIrrelevance.
 
 Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'.
 Proof.
-  intros n H.
-  dependent destruction H.
-  exists H ; exists a.
+  intros n v.
+  dependent destruction v.
+  exists v ; exists a.
   reflexivity.
 Save.
 
@@ -81,7 +81,7 @@ Qed.
 Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
 Proof with simpl in * ; simpl_depind ; auto.
   intros until 1.
-  dependent induction H generalizing Γ Δ α β...
+  dependent induction H generalizing Γ Δ α β.
 
   destruct Δ...
     apply weak ; apply ax.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 8e5729dce0..34fff9d186 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
 Axiom SetoidS1 : Setoid_Theory S1 eqS1.
 Add Setoid S1 eqS1 SetoidS1 as S1setoid.
 
-Instance DefaultRelation S1 eqS1.
+Instance eqS1_default : DefaultRelation S1 eqS1.
 
 Axiom eqS1': S1 -> S1 -> Prop.
 Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
 Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
 Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
 
-Instance DefaultRelation S1_test8 eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8.
 
 Axiom f_test8 : S2 -> S1_test8.
 Add Morphism f_test8 : f_compat_test8. Admitted.
-- 
cgit v1.2.3