X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Freduction%2Fifr.ma;h=fcc12edbf1c925c643b3e0839e3e13e41281c18b;hb=d7ff8dcf71f18a17fbf66696f0293cd411c1dbca;hp=a63368e1eb644b277899865c0a6ca8f43ca868a6;hpb=3bf7a0b4185dbffe5b822c907956acdbe2d1c559;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 a63368e1e..fcc12edbf 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma @@ -16,7 +16,6 @@ include "delayed_updating/unwind/unwind2_prototerm.ma". include "delayed_updating/substitution/fsubst.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". (* IMMEDIATE FOCUSED REDUCTION ************************************************)