X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fifr.ma;h=a63368e1eb644b277899865c0a6ca8f43ca868a6;hb=6c52017b15171aa20ddfd01c1bbf3cc22a86c81c;hp=87d855281d53c7a51c69608eee0700a69100ecff;hpb=4ac2becfaa45abb18acb2bdf3db5d2587cadb6d4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 87d855281..a63368e1e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -14,7 +14,7 @@
 
 include "delayed_updating/unwind/unwind2_prototerm.ma".
 include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
+include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
 include "delayed_updating/syntax/path_reverse.ma".
 include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".