- pts_dummy/pts_dummy_new: non compiling parts commented out

[helm.git] / matita / matita / lib / pts_dummy_new / convertibility.ma

diff --git a/matita/matita/lib/pts_dummy_new/convertibility.ma b/matita/matita/lib/pts_dummy_new/convertibility.ma
index 377d3c890488a0ab5907bfa302a3aa763839decf..23a9c686422c60c9806df7c17d8e3fdf7a8217ce 100644 (file)
--- a/matita/matita/lib/pts_dummy_new/convertibility.ma
+++ b/matita/matita/lib/pts_dummy_new/convertibility.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -71,3 +71,4 @@ theorem main1: ∀M,N. CO M N →
   |@(ex_intro … M) @(ex_intro … M) % // % //
   ]
 *)
+*)
\ No newline at end of file