]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma
- some refactoring and minor additions
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx_leq.ma
index cbc3365000129c3ccbdaab8be55a1eafe8f9a055..664688f7487ea2d516f4e937cfe6255de51c0efe 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/relocation/ldrop_leq.ma".
+include "basic_2/substitution/ldrop_leq.ma".
 include "basic_2/reduction/cpx.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)