dama, tests, legacy ported

[helm.git] / matita / tests / coercions_nonuniform.ma

diff --git a/matita/tests/coercions_nonuniform.ma b/matita/tests/coercions_nonuniform.ma
index 0cf156537a5c529c8268f9b87c5919775d39c75a..f21d82911cfaa9f03adc95bef258b2c0ea950253 100644 (file)
--- a/matita/tests/coercions_nonuniform.ma
+++ b/matita/tests/coercions_nonuniform.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/coercions_nonuniform/".
+
 
 axiom A : Type.
 axiom B : A -> Type.
@@ -21,7 +21,7 @@ axiom f1 : A -> A.
 
 axiom k : ∀a:A.B (f a).
 
-coercion cic:/matita/test/coercions_nonuniform/k.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/coercions_nonuniform/c1.con.
-coercion cic:/matita/test/coercions_nonuniform/c2.con.
+coercion cic:/matita/tests/coercions_nonuniform/c1.con.
+coercion cic:/matita/tests/coercions_nonuniform/c2.con.
 
 axiom g : C -> C.
 
@@ -43,4 +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
+*)