X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fcprop_connectives.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fcprop_connectives.ma;h=bd528521dba3e8ea456a501256f8f5f93ef91800;hb=aba6841906f09875a5800f58b24862444a1f4baf;hp=f9de36d1fa4a33fef91473d4f11d43bc86c0c7fd;hpb=8d367045e504f594c280d2c87f906695ef9671ee;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index f9de36d1f..bd528521d 100644
--- a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
@@ -62,7 +62,7 @@ interpretation "constructive quaternary and" 'and4 x y z t = (And4 x y z t).
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.
 
-record sigT (A:Type) (P:A→CProp) : Type ≝ {
+record sigT (A:Type) (P:A→Prop) : Type ≝ {
   fstT:A;
   sndT:P fstT
 }.