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

1 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index be7b77ef0..0db172e82 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.