X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Frtm_step.ma;h=e2d859b74bfac32601ffd7513cc3488566545091;hb=1555848a5546d0154964286d3400114481d78962;hp=5ca6add443d348d92279e20dbe94da507200ca96;hpb=548f2d3f410c05e2eb332f5c2d074f5e6c6985e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
index 5ca6add44..e2d859b74 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
@@ -36,7 +36,7 @@ inductive rtm_step: relation rtm ≝
 | rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
               rtm_step (mk_rtm (G. ⓛV) u E S (§p))
                        (mk_rtm G u E S V)
-| rtm_tau   : ∀G,u,E,S,W,T.
+| rtm_eps   : ∀G,u,E,S,W,T.
               rtm_step (mk_rtm G u E S (ⓝW. T))
                        (mk_rtm G u E S T)
 | rtm_appl  : ∀G,u,E,S,V,T.