X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fdivisible_group.ma;h=3789935502c97c448be4dced21f2d05bc58978df;hb=74769ee535a1a3f019e04da7501b183c15e348da;hp=3a79b11bbd969a884307f4a6a86d08e63cbcfff8;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma b/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma
index 3a79b11bb..378993550 100644
--- a/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma
@@ -20,8 +20,7 @@ include "group.ma".
 let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝
   match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m].
   
-interpretation "additive abelian group pow" 'times n x =
-  (cic:/matita/divisible_group/gpow.con _ x n).
+interpretation "additive abelian group pow" 'times n x = (gpow _ x n).
   
 record dgroup : Type ≝ {
   dg_carr:> abelian_group;
@@ -32,8 +31,7 @@ lemma divide: ∀G:dgroup.G → nat → G.
 intros (G x n); cases (dg_prop G x n); apply w; 
 qed.
 
-interpretation "divisible group divide" 'divide x n =
-  (cic:/matita/divisible_group/divide.con _ x n).
+interpretation "divisible group divide" 'divide x n = (divide _ x n).
 
 lemma divide_divides: 
   ∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x.