diff options
| author | msozeau | 2008-05-15 12:51:59 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-15 12:51:59 +0000 |
| commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
| tree | bd1ed746e255a9f25b486711163001b2f45d8017 /test-suite | |
| parent | a8b034513e0c03ceb7e154949b15f62ac6862f3b (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 8 | ||||
| -rw-r--r-- | test-suite/success/setoid_test2.v | 4 |
2 files changed, 6 insertions, 6 deletions
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. |