]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma
syntactic components detached from basic_2 become static_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx.ma
index da0bbe1ee7ef9a563bca8e2c6d39442be9ce4bb1..4c8371a0b74f9b8c748e9e9a35140b56ed215879 100644 (file)
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/predtystrong_5.ma".
-include "basic_2/syntax/tdeq.ma".
+include "static_2/syntax/tdeq.ma".
 include "basic_2/rt_transition/cpx.ma".
 
 (* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)