X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fattic%2Fordered_fields_ch0.ma;h=898148d6c4013b093e58ae42a11677538d620ead;hb=196d60526aaf4a10d0eaaf79cf8919c108b27a10;hp=b312c31ab6f43f7f8ea57484397b067dbc6c5206;hpb=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git

diff --git a/helm/software/matita/dama/attic/ordered_fields_ch0.ma b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
index b312c31ab..898148d6c 100644
--- a/helm/software/matita/dama/attic/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
@@ -12,13 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/ordered_fields_ch0/".
+
 
 include "attic/fields.ma".
 include "ordered_group.ma".
 
 (*CSC: non capisco questi alias! Una volta non servivano*)
-alias id "plus" = "cic:/matita/groups/plus.con".
+alias id "plus" = "cic:/matita/group/plus.con".
 alias symbol "plus" = "Abelian group plus".
 
 record pre_ordered_field_ch0: Type ≝
@@ -55,7 +55,7 @@ lemma of_ordered_abelian_group: pre_ordered_field_ch0 → ordered_abelian_group.
   ]
 qed.
 
-coercion cic:/matita/ordered_fields_ch0/of_ordered_abelian_group.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_ordered_abelian_group.con.
 
 (*CSC: I am not able to prove this since unfold is undone by coercion composition*)
 axiom of_with1:
@@ -74,7 +74,7 @@ lemma of_cotransitively_ordered_set : pre_ordered_field_ch0 → cotransitively_o
  ]
 qed.
 
-coercion cic:/matita/ordered_fields_ch0/of_cotransitively_ordered_set.con.
+coercion cic:/matita/attic/ordered_fields_ch0/of_cotransitively_ordered_set.con.
 
 record is_ordered_field_ch0 (F:pre_ordered_field_ch0) : Type \def
  { of_mult_compat: ∀a,b:F. 0≤a → 0≤b → 0≤a*b;