X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Frtm.ma;h=66b48129042f4055a37eacf3d13b55f248520c9b;hb=09b4420070d6a71990e16211e499b51dbb0742cb;hp=2e92ea0cca64f3d207b5610cacd8f2bb40a046f2;hpb=bba53a83579540bc3925d47d679e2aad22e85755;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma index 2e92ea0cc..66b481290 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/grammar/term_vector.ma". -include "basic_2/grammar/genv.ma". +include "basic_2/syntax/term_vector.ma". +include "basic_2/syntax/genv.ma". include "apps_2/functional/notation.ma". (* REDUCTION AND TYPE MACHINE ***********************************************)