qed => nqed.

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale_tests / micro_tests3.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma
index c6d6390d511a08a30cd6eff8e8ace55e41b998c8..71bd37984ff8c2b55ee17769f7e04b3cfbd3fb74 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/micro_tests3.ma
@@ -73,4 +73,4 @@ nlemma ok_mTest_HCS08_ROL_ROR_full :
            (mTest_HCS08_ROL_ROR_status t) (mk_word16 〈x1,x8〉 〈x6,xC〉)).
  #t; nelim t;
  napply refl_eq.
-qed.
+nqed.