models over N fixed

[helm.git] / helm / software / matita / contribs / dama / dama / cprop_connectives.ma

diff --git a/helm/software/matita/contribs/dama/dama/cprop_connectives.ma b/helm/software/matita/contribs/dama/dama/cprop_connectives.ma
index f9de36d1fa4a33fef91473d4f11d43bc86c0c7fd..bd528521dba3e8ea456a501256f8f5f93ef91800 100644 (file)
--- 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
 }.