X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fnotation.ma;h=dc4bda3964f7604728ef139cd78a4349153cdcce;hb=1efc4c2c7be1e4aff0ccccabf905d45795b3865f;hp=7be9b8ecbf4a0f71535470dc9cefc585fc762fdf;hpb=eca7393f8b871fd1d7838cfd5a176a80f4ec48c5;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index 7be9b8ecb..dc4bda396 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -192,7 +192,7 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $L $T1 $d $e $T2 }.
 
-(* Static Typing ************************************************************)
+(* Static typing ************************************************************)
 
 notation "hvbox( L ⊢ break term 90 T ÷ break A )"
    non associative with precedence 45
@@ -202,6 +202,16 @@ notation "hvbox( T1 ÷ ⊑ break T2 )"
    non associative with precedence 45
    for @{ 'CrSubEqA $T1 $T2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 • break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticType $h $L $T1 $T2 }.
+
+(* Unwind *******************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 •* break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticTypeStar $h $L $T1 $T2 }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( 𝐑 [ T ] )"
@@ -322,7 +332,7 @@ notation "hvbox( T1 ⊢ ⬌* break T2 )"
    non associative with precedence 45
    for @{ 'CPConvStar $T1 $T2 }.
 
-(* Native typing ************************************************************)
+(* Dynamic typing ***********************************************************)
 
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
    non associative with precedence 45