- degree-based equivalene for terms

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / functional / rtm.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma
index 2e92ea0cca64f3d207b5610cacd8f2bb40a046f2..66b48129042f4055a37eacf3d13b55f248520c9b 100644 (file)
--- 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 ***********************************************)