snapshot

[helm.git] / helm / software / matita / dama / attic / ordered_fields_ch0.ma

diff --git a/helm/software/matita/dama/attic/ordered_fields_ch0.ma b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
index b312c31ab6f43f7f8ea57484397b067dbc6c5206..898148d6c4013b093e58ae42a11677538d620ead 100644 (file)
--- 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;