Non working parts of the library commented out.

[helm.git] / matita / matita / lib / arithmetics / sigma_pi.ma

diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index d92d525b7c37b9c5c200c6f5a6ffc15db8a974b5..94b3794b3f08345bad1d83896e5b88ed2d737f43 100644 (file)
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -9,6 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
+(* To be ported
 include "arithmetics/bigops.ma".
 
 definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 
@@ -744,4 +745,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y
     |assumption
     ]
   ]
-qed. *)
\ No newline at end of file
+qed. *)*)
\ No newline at end of file