X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Fcube.ma;h=c143261ad5fe18c398ff6da0517bcae05278f1dc;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=8ac3d978c74f5e6a889cdcc155916c19cf084380;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

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