- lambda: parallel reduction to obtain diamond property

[helm.git] / matita / matita / contribs / lambda / redex_pointer.ma

diff --git a/matita/matita/contribs/lambda/redex_pointer.ma b/matita/matita/contribs/lambda/redex_pointer.ma
index f6e05c93fa740e664bad3e766e73cde027eb232d..6895ea787e5440f07250c2799b8607fed6313a56 100644 (file)
--- 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).