update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
index e79ed15f5c1ddde35203bdd51b62399cd0e63845..88924f4e084ded5a16ad1c58d32ce504d9edf747 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma
@@ -16,12 +16,12 @@ include "ground_2/lib/star.ma".
 include "basic_2/notation/relations/predtystar_5.ma".
 include "basic_2/rt_transition/cpx.ma".
 
-(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************)
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
 
 definition cpxs: sh → relation4 genv lenv term term ≝
                  λh,G. CTC … (cpx h G).
 
-interpretation "uncounted context-sensitive parallel rt-computation (term)"
+interpretation "unbound context-sensitive parallel rt-computation (term)"
    'PRedTyStar h G L T1 T2 = (cpxs h G L T1 T2).
 
 (* Basic eliminators ********************************************************)