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

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma
index 728f48df97bc855c2f108f127daf3324674de784..deaa7a967ec39570fb0bda6a6adba517641e20be 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/relocation/lleq_lleq.ma".
 include "basic_2/computation/lpxs_lpxs.ma".
 include "basic_2/computation/fpns.ma".