- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy_new/arity_eval.ma b/matita/matita/lib/pts_dummy_new/arity_eval.ma
index 6fcf0e0c0ef76691462108ca89d46d1934905935..8adcc4873020bb93bb30afecd4f6559305a416bd 100644 (file)
--- a/matita/matita/lib/pts_dummy_new/arity_eval.ma
+++ b/matita/matita/lib/pts_dummy_new/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.
 *)
+*)