X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fcoercions_nonuniform.ma;h=f21d82911cfaa9f03adc95bef258b2c0ea950253;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=bed1d73dc6f54ba5c5f491d13d26ad82698e67e5;hpb=31cd60ef97eb2b90791b1470f389544de788bcd1;p=helm.git

diff --git a/helm/software/matita/tests/coercions_nonuniform.ma b/helm/software/matita/tests/coercions_nonuniform.ma
index bed1d73dc..f21d82911 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/".
+
 
 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/tests/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/tests/coercions_nonuniform/c1.con.
+coercion cic:/matita/tests/coercions_nonuniform/c2.con.
 
 axiom g : C -> C.
 
@@ -44,6 +44,3 @@ definition test := λa:A.g a.
 Coq < Coercion c1 : B >-> C.                
 User error: c1 does not respect the inheritance uniform condition
 *)
-
-
-