1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / micro_tests.ma

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 a135d153a55af0afdf785338bd2f27f0e163509a..0f75a3f2f8be4686dd1390df91e14355c979e8fb 100755 (executable)
--- 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.
 
 (* ********* *)