X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fhints_declaration.ma;h=27330da468fb49b2c9bdcbc1a6161ae8f17ce29a;hb=f12f1b61a608140a65990d36045d978575b2dcb0;hp=dac148e4fe9f80f99fbd3fef5dc3e733c101d335;hpb=bc4cc41e813fc850a7f981cd60ba22e14485b7d1;p=helm.git

diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma
index dac148e4f..27330da46 100644
--- a/helm/software/matita/nlibrary/hints_declaration.ma
+++ b/helm/software/matita/nlibrary/hints_declaration.ma
@@ -37,7 +37,7 @@ With unidoce and some ASCII art it looks like the following:
 *)
    
 (* it seems unbelivable, but it works! *)
-notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 90 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
+notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
   with precedence 90
   for @{ ${ fold right 
                @{ ${ default 
@@ -57,10 +57,10 @@ include "logic/pts.ma".
 
 ndefinition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
 ndefinition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
-ndefinition hint_declaration_Type2  ≝  λa,b:Type[1].Prop.
+ndefinition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
 ndefinition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
 ndefinition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
-ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[1].Prop.
+ndefinition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
   
 interpretation "hint_decl_Type2"  'hint_decl a b = (hint_declaration_Type2 a b).
 interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).