matitadep sould be ok, outputs warning regarding issues and

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

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