X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Ftypes.ma;h=a5e35c9d218a5d756319dd429dd7e1b6d4e8363e;hb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;hp=94777e0710e6c28e230c1e407426c1b62ce3e8b6;hpb=30172d86a0cd979e44ae3343655f6ce55043dd52;p=helm.git

diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 94777e071..a5e35c9d2 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -67,7 +67,7 @@ interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
 
 (* sigma *)
 record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
-    pi1: A
+    pi1: A  (* not a coercion due to problems with Cerco *)
   ; pi2: f pi1
   }.