X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fattic%2Fordered_fields_ch0.ma;h=898148d6c4013b093e58ae42a11677538d620ead;hb=db068aa35cc47bb881ec810bf3b904c3d7cc9379;hp=5be3c9da49eaea573feb1723c19d33f9635f1ca3;hpb=df666eb58afe0b312a2c4d41683d7ae4828ee8bd;p=helm.git

diff --git a/matita/dama/attic/ordered_fields_ch0.ma b/matita/dama/attic/ordered_fields_ch0.ma
index 5be3c9da4..898148d6c 100644
--- a/matita/dama/attic/ordered_fields_ch0.ma
+++ b/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;