X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmicro_tests.ma;h=0f75a3f2f8be4686dd1390df91e14355c979e8fb;hb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;hp=a135d153a55af0afdf785338bd2f27f0e163509a;hpb=96881c08dcd617524621fb2f241fe38da81f2083;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma
index a135d153a..0f75a3f2f 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma
@@ -186,7 +186,7 @@ nlemma ok_mTest_HCS08_ADC_full :
   | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]);
  normalize in AFTER_ALU8:(%); *) 
 
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 (* ********* *)