Some notes for Enrico.

[helm.git] / matita / dama / ordered_groups.ma

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index cff205ce9a267a3eaa791f4ccf2b347cbead6140..cc7e739280cbbd58e277850e2c300e1fe350da88 100644 (file)
--- 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