]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/lib/pts_dummy_new/terms.ma
- pts_dummy/pts_dummy_new: non compiling parts commented out
[helm.git] / matita / matita / lib / pts_dummy_new / terms.ma
index 0227f1e948e3787f6269b58c252f5558b427ad8d..1291013ffd79807624d9ee4fb85db946f3e54a21 100644 (file)
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
 
 inductive T : Type[0] ≝
   | Sort: nat → T     (* starts from 0 *)