X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fhints_declaration.ma;h=588741fa32c45d4f316fe663849e8a49f90dae5b;hb=d02c188ee3d4bd9885490447e63453adb2cb4ea1;hp=d04f453f2adad0ffa376932aaf26ccbd42ba15bc;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/hints_declaration.ma b/weblib/hints_declaration.ma
index d04f453f2..588741fa3 100644
--- a/weblib/hints_declaration.ma
+++ b/weblib/hints_declaration.ma
@@ -58,12 +58,12 @@ notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (lis
 
 include "basics/pts.ma".
 
-definition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
-definition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
-definition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
-definition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
-definition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
-definition hint_declaration_CProp2 ≝  λa,b:CProp[2].Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_Type0"definition hint_declaration_Type0  ≝  λA:Type[0] .λa,b:A.Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_Type1"definition hint_declaration_Type1  ≝  λA:Type[1].λa,b:A.Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_Type2"definition hint_declaration_Type2  ≝  λa,b:Type[2].Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_CProp0"definition hint_declaration_CProp0 ≝  λA:CProp[0].λa,b:A.Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_CProp1"definition hint_declaration_CProp1 ≝  λA:CProp[1].λa,b:A.Prop.
+img class="anchor" src="icons/tick.png" id="hint_declaration_CProp2"definition 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).