diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-07 20:27:24 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-07 20:27:24 +0000 |
| commit | c63367d05354834211cadb38340334960e8106f8 (patch) | |
| tree | 29af35131d7857fc860c1ef381c3e5f6d4dfaa21 /test-suite/success | |
| parent | a20115809c0c6a36124366fae64130e3e513c1f1 (diff) | |
Fix implicit arguments in sections bug and check for resolution of evars when
defining records. Fix test-suite script because of new implicit argument
setting for DefaultRelation. Fix regression in auto, changing the order
of tried lemmas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
| -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 34fff9d18..b89787bb0 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 eqS1_default : DefaultRelation S1 eqS1. +Instance eqS1_default : DefaultRelation 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 eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8. +Instance eqS1_test8_default : DefaultRelation eqS1_test8. Axiom f_test8 : S2 -> S1_test8. Add Morphism f_test8 : f_compat_test8. Admitted. |