From ec9b3b8174737fd672110965cb971521ef897ecb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Aug 2007 09:00:19 +0000 Subject: [PATCH] baseuri changed --- .../software/matita/tests/coercions_nonuniform.ma | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/tests/coercions_nonuniform.ma b/helm/software/matita/tests/coercions_nonuniform.ma index bed1d73dc..0cf156537 100644 --- a/helm/software/matita/tests/coercions_nonuniform.ma +++ b/helm/software/matita/tests/coercions_nonuniform.ma @@ -12,16 +12,16 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". +set "baseuri" "cic:/matita/test/coercions_nonuniform/". axiom A : Type. axiom B : A -> Type. axiom f : A -> A. axiom f1 : A -> A. -axiom c : ∀a:A.B (f a). +axiom k : ∀a:A.B (f a). -coercion cic:/matita/test/c.con. +coercion cic:/matita/test/coercions_nonuniform/k.con. axiom C : Type. @@ -33,8 +33,8 @@ axiom C : Type. axiom c2 : ∀a.B (f a) -> B (f1 a). axiom c1 : ∀a:A. B (f1 a) -> C. -coercion cic:/matita/test/c1.con. -coercion cic:/matita/test/c2.con. +coercion cic:/matita/test/coercions_nonuniform/c1.con. +coercion cic:/matita/test/coercions_nonuniform/c2.con. axiom g : C -> C. @@ -43,7 +43,4 @@ definition test := λa:A.g a. (* Coq < Coercion c1 : B >-> C. User error: c1 does not respect the inheritance uniform condition -*) - - - +*) \ No newline at end of file -- 2.39.2