- intermediate commit to allow debugging of auto tactic in xprs.ma

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

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
index 9a04c807041a46972bbfae728301d3984b5de430..bf04f72c9e53828ba58f849a747252fc9ce2c57f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
@@ -37,7 +37,7 @@ inductive rtm_step: relation rtm ≝
               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_step (mk_rtm G u E S (â\93£W. T))
+              rtm_step (mk_rtm G u E S (â\93\9dW. T))
                        (mk_rtm G u E S T)
 | rtm_appl  : ∀G,u,E,S,V,T.
               rtm_step (mk_rtm G u E S (ⓐV. T))