diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
| commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
| tree | bd1ed746e255a9f25b486711163001b2f45d8017 /test-suite/success/setoid_test2.v | |
| 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/success/setoid_test2.v')
| -rw-r--r-- | test-suite/success/setoid_test2.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 8e5729dce..34fff9d18 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. |