X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=34661dc8015e62a19403fb16e337359acb59c19e;hb=8cb2490b5b202549a596cfd1d0f166a5ee43fc4e;hp=a149bc9ddf4e88133871e0d73aed62fe02fb613b;hpb=12bebae6f57b3a671a1aa29662d5ed7208a85667;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index a149bc9dd..34661dc80 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -14,38 +14,38 @@
 
 include "logic/pts.ma".
 
-ninductive True: CProp ≝
+ninductive True: CProp[0] ≝
   I : True.
 
-ninductive False: CProp ≝.
+ninductive False: CProp[0] ≝.
 
-ndefinition Not: CProp → CProp ≝
+ndefinition Not: CProp[0] → CProp[0] ≝
   λA. A → False.
 
 interpretation "logical not" 'not x = (Not x).
 
-ninductive And (A,B:CProp) : CProp ≝
+ninductive And (A,B:CProp[0]) : CProp[0] ≝
     conj : A → B → And A B.
 
 interpretation "logical and" 'and x y = (And x y).
 
-ninductive Or (A,B:CProp) : CProp ≝
+ninductive Or (A,B:CProp[0]) : CProp[0] ≝
      or_introl : A → Or A B
    | or_intror : B → Or A B.
 
 interpretation "logical or" 'or x y = (Or x y).
 
-ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
+ninductive Ex (A:Type[0]) (P:A → CProp[0]) : CProp[0] ≝
     ex_intro: ∀x:A. P x → Ex A P.
 
 
-ninductive Ex1 (A:Type[1]) (P:A → CProp) : CProp[1] ≝
+ninductive Ex1 (A:Type[1]) (P:A → CProp[0]) : CProp[1] ≝
     ex_intro1: ∀x:A. P x → Ex1 A P.
 
 interpretation "exists1" 'exists x = (Ex1 ? x).
 interpretation "exists" 'exists x = (Ex ? x).
 
-nrecord iff (A,B: CProp) : CProp ≝
+nrecord iff (A,B: CProp[0]) : CProp[0] ≝
  { if: A → B;
    fi: B → A
  }.