X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fredex_pointer.ma;h=6895ea787e5440f07250c2799b8607fed6313a56;hb=6b87a3e9d6dd7c3abb922750587444ac3fd08e16;hp=f6e05c93fa740e664bad3e766e73cde027eb232d;hpb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;p=helm.git

diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
index f6e05c93f..6895ea787 100644
--- a/matita/matita/contribs/lambda/redex_pointer.ma
+++ b/matita/matita/contribs/lambda/redex_pointer.ma
@@ -47,6 +47,6 @@ notation "hvbox(a break ≺ b)"
 interpretation "'less than' on redex pointers"
    'lt p q = (TC rpointer rpprec p q).
 
-(* Note: this is p ≤ q, that *really* is p < q ∨ p = q *)
+(* Note: this is p ≤ q *)
 interpretation "'less or equal to' on redex pointers"
-   'leq x y = (RC rpointer (TC rpointer rpprec) x y).
+   'leq x y = (star rpointer x y).