X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc.ma;h=62228d229e21af156c36c43980e8956f51a4fd48;hb=f6b452b9c9be141740d4058dfbcf81a4b75fd00b;hp=494650d04d9dff70e6bff2054b0aa538d2613ef5;hpb=88dd0e28758c693660a93ee0a9a5202c61ca09a0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
index 494650d04..62228d229 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma
@@ -22,13 +22,13 @@ include "ground_2/lib/arith.ma".
 
 record rtc: Type[0] ≝ {
    ri: nat; (* Note: inner r-steps *)
-   rh: nat; (* Note: head  r-steps *)
+   rs: nat; (* Note: spine r-steps *)
    ti: nat; (* Note: inner t-steps *)
-   th: nat  (* Note: head  t-steps *)
+   ts: nat  (* Note: spine t-steps *)
 }.
 
 interpretation "constructor (rtc)"
-   'Tuple ri rh ti th = (mk_rtc ri rh ti th).
+   'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
 
 interpretation "one structural step (rtc)"
    'ZeroZero = (mk_rtc O O O O).