- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy/arity.ma b/matita/matita/lib/pts_dummy/arity.ma
index 3df7811c060e003335a8f36fb3dc3ac0badfc7cc..b5dd81df710cd84e4627e9a5dd04093a27be283d 100644 (file)
--- a/matita/matita/lib/pts_dummy/arity.ma
+++ b/matita/matita/lib/pts_dummy/arity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
 (* ARITIES ********************************************************************)
 
 (* An arity is a normal term representing the functional structure of a term.
@@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
 #E1 #E2 #H #i @(all2_nth … aeq) //
 qed.
+*)