nasty change in the lexer/parser:

[helm.git] / helm / software / matita / library / algebra / finite_groups.ma

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 36573a8a7d0598217d5cae8cb8c00c9d01ffc8b4..6da0a7256b0eb0517ca203228041d58a4e6ed72e 100644 (file)
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -29,9 +29,9 @@ for @{ 'repr $C $i }.
 
 (* CSC: multiple interpretations in the same file are not considered in the
  right order
-interpretation "Finite_enumerable representation" 'repr C i = (repr C _ i).*)
+interpretation "Finite_enumerable representation" 'repr C i = (repr C ? i).*)
  
-interpretation "Finite_enumerable order" 'card C = (order C _).
+interpretation "Finite_enumerable order" 'card C = (order C ?).
 
 record finite_enumerable_SemiGroup : Type≝
  { semigroup:> SemiGroup;
@@ -47,7 +47,7 @@ for @{ 'index_of_finite_enumerable_semigroup $e }.
 interpretation "Index_of_finite_enumerable representation"
  'index_of_finite_enumerable_semigroup e
 =
- (index_of _ (is_finite_enumerable _) e).
+ (index_of ? (is_finite_enumerable ?) e).
 
 
 (* several definitions/theorems to be moved somewhere else *)