X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fordered_groups.ma;h=cc7e739280cbbd58e277850e2c300e1fe350da88;hb=fbfc3e402894a89b22f57e12b53e090f843a690a;hp=cff205ce9a267a3eaa791f4ccf2b347cbead6140;hpb=db929143eeb0c6e33323c0614d4c8f01817fbca0;p=helm.git

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index cff205ce9..cc7e73928 100644
--- a/matita/dama/ordered_groups.ma
+++ b/matita/dama/ordered_groups.ma
@@ -32,7 +32,9 @@ qed.
 
 coercion cic:/matita/ordered_groups/og_abelian_group.con.
 
-
+(* CSC: NO! Cosi' e' nel frammento negativo. Devi scriverlo con l'eccedenza!
+   Tutto il resto del file e' da rigirare nel frammento positivo.
+*)
 record ogroup : Type ≝ { 
   og_carr:> pre_ogroup;
   fle_plusr: ∀f,g,h:og_carr. f≤g → f+h≤g+h