X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Flibrary_auto%2Fauto%2Fnat%2Fdiv_and_mod.ma;h=d81a0a1cf8c127c413334d26b3241637fb21198b;hb=b714e87e96f14f332a5157567a4c62a4b28fa8eb;hp=bbb3d49b1c32a13721e9bc3b996d628aedd9f6a4;hpb=bbb9215a02e1321d01a11c0ead6d0d218d047f68;p=helm.git

diff --git a/helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma b/helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma
index bbb3d49b1..d81a0a1cf 100644
--- a/helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma
+++ b/helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma
@@ -31,8 +31,7 @@ match m with
 [O \Rightarrow m
 | (S p) \Rightarrow mod_aux n n p]. 
 
-interpretation "natural remainder" 'module x y =
-  (cic:/matita/library_autobatch/nat/div_and_mod/mod.con x y).
+interpretation "natural remainder" 'module x y = (mod x y).
 
 let rec div_aux p m n : nat \def
 match (leb m n) with
@@ -48,8 +47,7 @@ match m with
 [O \Rightarrow S n
 | (S p) \Rightarrow div_aux n n p]. 
 
-interpretation "natural divide" 'divide x y =
-  (cic:/matita/library_autobatch/nat/div_and_mod/div.con x y).
+interpretation "natural divide" 'divide x y = (div x y).
 
 theorem le_mod_aux_m_m: 
 \forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.