update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / ibfr_unwind.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
index 34feec2432c419cfa282e917b6c92e56f71aaeb8..56cfaa6ca060b2277cfcc83248403697476f6121 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
@@ -14,10 +14,10 @@
 
 include "delayed_updating/reduction/ibfr.ma".
 
-include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
-include "delayed_updating/unwind/unwind2_preterm_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_crux.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_fsubst.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm_lift.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_crux.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".