]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_lift.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / dbfr_lift.ma
index fc67c5779640106caa7c7f49f6ea1a4d9299ee4c..0c6ab932f53d5e67689f601148b34f42ddae92a6 100644 (file)
@@ -16,7 +16,7 @@ include "delayed_updating/reduction/dbfr.ma".
 
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_constructors.ma".
+include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_path_structure.ma".
 include "delayed_updating/substitution/lift_path_closed.ma".
 include "delayed_updating/substitution/lift_rmap_closed.ma".