X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Fcoercions.ma;h=914126de2454d4804dfc6909837254f6d6417c68;hb=872dbd15c8f6d10c2b9b46ad6f995bf494c23e65;hp=20b15cd2650d8a7f7840d68696da39423af2248c;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma
index 20b15cd26..914126de2 100644
--- a/matita/tests/coercions.ma
+++ b/matita/tests/coercions.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/coercions/".
-include "legacy/coq.ma".
+include "nat/nat.ma".
 
 inductive pos: Set \def
 | one : pos
@@ -61,4 +61,26 @@ definition double2:
 \def 
   \lambda f:int \to int. \lambda x : pos .f (nat2int (pos2nat x)).
   
-  
+coercion cic:/matita/logic/equality/eq_f.con.  
+coercion cic:/matita/logic/equality/eq_f1.con.
+variant xxx : ? \def eq_f.
+coercion cic:/matita/tests/coercions/xxx.con.
+
+theorem coercion_svelta : \forall T,S:Type.\forall f:T \to S.\forall x,y:T.x=y \to f y = f x.
+  intros.
+  apply ((\lambda h:f y = f x.h) H).
+qed.
+
+variant pos2nat' : ? \def pos2nat.
+
+coercion cic:/matita/tests/coercions/xxx.con.
+
+inductive initial: Set \def iii : initial.
+
+definition i2pos: ? \def \lambda x:initial.one.
+
+coercion cic:/matita/tests/coercions/i2pos.con.
+
+coercion cic:/matita/tests/coercions/pos2nat'.con.
+
+