nasty change in the lexer/parser:

[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 3789935502c97c448be4dced21f2d05bc58978df..d751e9ba274f9934a5f08bb6fd5dc65891498a15 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,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.