X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Faux_bases.ma;h=f2d2a5ce5a458067366f4a31c1dcee2c26c9981f;hb=be527f5bd4acaf530d8843b23e6849fd5211e1fc;hp=50314e9b179e5699a22944a78195986c4b3a050d;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/assembly/freescale/aux_bases.ma
index 50314e9b1..f2d2a5ce5 100644
--- a/helm/software/matita/contribs/assembly/freescale/aux_bases.ma
+++ b/helm/software/matita/contribs/assembly/freescale/aux_bases.ma
@@ -47,7 +47,7 @@ definition exadecim_of_oct ≝
   [ o0 ⇒ x0 | o1 ⇒ x1 | o2 ⇒ x2 | o3 ⇒ x3
   | o4 ⇒ x4 | o5 ⇒ x5 | o6 ⇒ x6 | o7 ⇒ x7 ].
 
-coercion cic:/matita/freescale/aux_bases/exadecim_of_oct.con.
+coercion exadecim_of_oct.
 
 (* iteratore sugli ottali *)
 definition forall_oct ≝ λP.
@@ -104,7 +104,7 @@ definition byte8_of_bitrigesim ≝
   | t18 ⇒ 〈x1,x8〉 | t19 ⇒ 〈x1,x9〉 | t1A ⇒ 〈x1,xA〉 | t1B ⇒ 〈x1,xB〉
   | t1C ⇒ 〈x1,xC〉 | t1D ⇒ 〈x1,xD〉 | t1E ⇒ 〈x1,xE〉 | t1F ⇒ 〈x1,xF〉 ].
 
-coercion cic:/matita/freescale/aux_bases/byte8_of_bitrigesim.con.
+coercion byte8_of_bitrigesim.
 
 (* iteratore sui bitrigesimali *)
 definition forall_bitrigesim ≝ λP.