reaxiomatized lleq fixes a bug in it and allows to park substitution in etc

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsx_ldrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
index 61466ca351f3771d8c0ba8b57d033dd5ea14f74f..9bd29a5f1964214ddcb5351cfc52c954a4c8cbfd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/relocation/lleq_ldrop.ma".
 include "basic_2/computation/lpxs_ldrop.ma".
 include "basic_2/computation/lsx.ma".