a) update with upstream version

[helm.git] / helm / software / matita / contribs / dama / dama_duality / divisible_group.ma

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 3a79b11bbd969a884307f4a6a86d08e63cbcfff8..3789935502c97c448be4dced21f2d05bc58978df 100644 (file)
--- 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.