- ldrop is now drop as in basic_1

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / functional / rtm_step.ma

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 e2d859b74bfac32601ffd7513cc3488566545091..ed77ca726169ed4b3531358b44775d08a7dce708 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma
@@ -18,7 +18,7 @@ include "apps_2/functional/rtm.ma".
 
 (* transitions *)
 inductive rtm_step: relation rtm ≝
-| rtm_ldrop : ∀G,u,E,I,t,D,V,S,i.
+| rtm_drop : ∀G,u,E,I,t,D,V,S,i.
               rtm_step (mk_rtm G u (E. ④{I} {t, D, V}) S (#(i + 1)))
                        (mk_rtm G u E S (#i))
 | rtm_ldelta: ∀G,u,E,t,D,V,S.