X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Farity_eval.ma;h=8adcc4873020bb93bb30afecd4f6559305a416bd;hb=d9a1ff8259a7882caa0ffd27282838c00a34cab5;hp=6fcf0e0c0ef76691462108ca89d46d1934905935;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/arity_eval.ma b/matita/matita/lib/pts_dummy/arity_eval.ma
index 6fcf0e0c0..8adcc4873 100644
--- a/matita/matita/lib/pts_dummy/arity_eval.ma
+++ b/matita/matita/lib/pts_dummy/arity_eval.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/arity.ma".
-
+include "pts_dummy/arity.ma".
+(*
 (* ARITY ASSIGNMENT ***********************************************************)
 
 (* the arity type *************************************************************)
@@ -226,3 +226,4 @@ axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2
 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
 @A qed.
 *)
+*)