- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy/par_reduction.ma b/matita/matita/lib/pts_dummy/par_reduction.ma
index cea1e177b8ed33fc04202bf2b2ba9fe3601cb1f3..fec59888c23b963eda89b720868ddb2a348473cb 100644 (file)
--- a/matita/matita/lib/pts_dummy/par_reduction.ma
+++ b/matita/matita/lib/pts_dummy/par_reduction.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subterms.ma".
-
+include "pts_dummy/subterms.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -305,3 +305,4 @@ pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
 
+*)