- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy/types.ma b/matita/matita/lib/pts_dummy/types.ma
index 0c07d2e70408d3e76c01a88e3a0094447dce62e6..acc0c8b135f0ed386273087989615328662ce807 100644 (file)
--- a/matita/matita/lib/pts_dummy/types.ma
+++ b/matita/matita/lib/pts_dummy/types.ma
@@ -9,10 +9,10 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subst.ma".
-include "basics/list.ma".
-
+include "pts_dummy/subst.ma".
+include "basics/lists/list.ma".
 
+(*
 (*************************** substl *****************************)
 
 let rec substl (G:list T) (N:T) : list T ≝  
@@ -190,3 +190,4 @@ lemma tj_subst_0: ∀P,G,v,w. G ⊢_{P} v : w → ∀t,u. w :: G ⊢_{P} t : u 
 #P #G #v #w #Hv #t #u #Ht 
 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 qed.
+*)