From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- test-suite/success/setoid_test2.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test-suite/success/setoid_test2.v') diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 34fff9d1..b89787bb 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. -- cgit v1.2.3