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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma
index 9f5111ad2ce6c506cdca1098ad09a0b0cd284ef4..863b08196e3f88011eaf6ab20e5262fe66674335 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/relocation/lleq_lleq.ma".
 include "basic_2/computation/cpxs_lleq.ma".
 include "basic_2/computation/lpxs_lleq.ma".
 include "basic_2/computation/lpxs_lpxs.ma".