X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Fcube.ma;fp=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Fcube.ma;h=c143261ad5fe18c398ff6da0517bcae05278f1dc;hb=dbd9f7d4de8286fdd54f4b5609576f33db1050a6;hp=8ac3d978c74f5e6a889cdcc155916c19cf084380;hpb=716338697e54d7a7e3602aabdecc2a8a639d683e;p=helm.git

diff --git a/matita/matita/lib/pts_dummy_new/cube.ma b/matita/matita/lib/pts_dummy_new/cube.ma
index 8ac3d978c..c143261ad 100644
--- a/matita/matita/lib/pts_dummy_new/cube.ma
+++ b/matita/matita/lib/pts_dummy_new/cube.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "convertibility.ma".
-include "types.ma".
-
+include "pts_dummy/convertibility.ma".
+include "pts_dummy/types.ma".
+(*
 (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
 
 inductive Cube_Ax: nat → nat → Prop ≝
@@ -41,3 +41,4 @@ inductive FO_Re: nat → nat → nat → Prop ≝
 .
 
 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
+*)