X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fdivisible_group.ma;h=d751e9ba274f9934a5f08bb6fd5dc65891498a15;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=3789935502c97c448be4dced21f2d05bc58978df;hpb=9eabe046c1182960de8cfdba96c5414224e3a61e;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 378993550..d751e9ba2 100644
--- a/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/divisible_group.ma
@@ -20,7 +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 = (gpow _ x n).
+interpretation "additive abelian group pow" 'times n x = (gpow ? x n).
   
 record dgroup : Type ≝ {
   dg_carr:> abelian_group;
@@ -31,7 +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 = (divide _ 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.