X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Freduction.ma;h=66bcd28903c9f9aa1b992b7db3e06c0dff0728a2;hb=be80aa40b9a66d5b12f92d03c2aa7b1dd8e49893;hp=58e4e179aab1ff9e6f8fa935d257bf0749c9125e;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/reduction.ma b/matita/matita/lib/pts_dummy/reduction.ma
index 58e4e179a..66bcd2890 100644
--- 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.
-
-
-
-
+*)