]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / reduction / dbfr_ibfr.ma
index eee619916365c16cbad2af6094e405dd46e5c6fc..35966d9f7983a5f245f06d38246928b4f9f6f7c6 100644 (file)
@@ -15,7 +15,7 @@
 include "delayed_updating/reduction/dbfr.ma".
 include "delayed_updating/reduction/ibfr.ma".
 
-include "delayed_updating/unwind/unwind2_constructors.ma".
+include "delayed_updating/unwind/unwind2_prototerm_constructors.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".