a) update with upstream version

[helm.git] / helm / software / matita / contribs / assembly / freescale / aux_bases.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/aux_bases.ma b/helm/software/matita/contribs/assembly/freescale/aux_bases.ma
index 50314e9b179e5699a22944a78195986c4b3a050d..f2d2a5ce5a458067366f4a31c1dcee2c26c9981f 100644 (file)
--- 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.