X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Fcprs.ma;h=42b5b362162b01e0d5abd62e5985a36fe4adc656;hp=8d71a75c48af85007a93b2651c13b3a8fda453d8;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs.ma
index 8d71a75c4..42b5b3621 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/cprs.ma
@@ -19,7 +19,7 @@ include "basic_2A/reduction/cnr.ma".
 
 (* Basic_1: includes: pr1_pr0 *)
 definition cprs: relation4 genv lenv term term ≝
-                 λG. LTC … (cpr G).
+                 λG. CTC … (cpr G).
 
 interpretation "context-sensitive parallel computation (term)"
    'PRedStar G L T1 T2 = (cprs G L T1 T2).
@@ -60,7 +60,7 @@ lemma cprs_strap2: ∀G,L,T1,T,T2.
 normalize /2 width=3 by TC_strap/ qed-.
 
 lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
-/3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
+/3 width=5 by lsubr_cpr_trans, CTC_lsub_trans/
 qed-.
 
 (* Basic_1: was: pr3_pr1 *)