- pts_dummy/pts_dummy_new: non compiling parts commented out

[helm.git] / matita / matita / lib / pts_dummy / cube.ma

diff --git a/matita/matita/lib/pts_dummy/cube.ma b/matita/matita/lib/pts_dummy/cube.ma
index 8ac3d978c74f5e6a889cdcc155916c19cf084380..c143261ad5fe18c398ff6da0517bcae05278f1dc 100644 (file)
--- a/matita/matita/lib/pts_dummy/cube.ma
+++ b/matita/matita/lib/pts_dummy/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.
+*)