we are moving the devel root one dir level up

[helm.git] / helm / software / matita / library / freescale / medium_tests.ma

diff --git a/helm/software/matita/library/freescale/medium_tests.ma b/helm/software/matita/library/freescale/medium_tests.ma
index 41cc96ae9ccfcfe255853171d788a09758f3e990..91e185b6f3fb42a59dc42189946a4920b0865364 100644 (file)
--- a/helm/software/matita/library/freescale/medium_tests.ma
+++ b/helm/software/matita/library/freescale/medium_tests.ma
@@ -195,7 +195,7 @@ lemma dTest_HCS08_sReverse_aux ≝
    | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_bytes 〈〈x0,xD〉:〈x0,x0〉〉))
    ] =
   Some ? (set_pc_reg HCS08 t
-   (dTest_HCS08_sReverse_status t (fstT ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string)) 
+   (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string)) 
    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 
 (* dimostrazione senza svolgimento degli stati *)