]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/basics/types.ma
typos
[helm.git] / matita / matita / lib / basics / types.ma
index 94777e0710e6c28e230c1e407426c1b62ce3e8b6..b319b5bd09907332f1d9ff2cea3b3bac02dedb25 100644 (file)
@@ -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
   ; pi2: f pi1
   }.