- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy/reduction.ma b/matita/matita/lib/pts_dummy/reduction.ma
index 58e4e179aab1ff9e6f8fa935d257bf0749c9125e..66bcd28903c9f9aa1b992b7db3e06c0dff0728a2 100644 (file)
--- a/matita/matita/lib/pts_dummy/reduction.ma
+++ b/matita/matita/lib/pts_dummy/reduction.ma
@@ -9,9 +9,9 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/par_reduction.ma".
+include "pts_dummy/par_reduction.ma".
 include "basics/star.ma".
-
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -353,7 +353,4 @@ lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
    @red_subst1 //
   ]
 qed.
-
-
-
-
+*)