X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fsigma_pi.ma;h=94b3794b3f08345bad1d83896e5b88ed2d737f43;hb=2f5b8ded5e2ef21f1bead554f4dd42759f2f9972;hp=d92d525b7c37b9c5c200c6f5a6ffc15db8a974b5;hpb=7ad16d18416a08382d62747fce4a0ac18ee557e0;p=helm.git

diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index d92d525b7..94b3794b3 100644
--- 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