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=cf07c50b03a49344eb4cbe2e1bc18fcef880b9e9;hp=5be3c9da49eaea573feb1723c19d33f9635f1ca3;hpb=39c55604f8114e2e8f9f9769acd328de8f19c7e4;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 5be3c9da4..898148d6c 100644
--- a/helm/software/matita/dama/attic/ordered_fields_ch0.ma
+++ b/helm/software/matita/dama/attic/ordered_fields_ch0.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/ordered_fields_ch0/".
+
 
 include "attic/fields.ma".
 include "ordered_group.ma".
@@ -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;