Fix error-msg-tests

src/verification/FPSProp.v

@@ -496,7 +496,6 @@ Module FPS_PROP (EVAL_Def: EVAL_ENV)
     Qed.
 
     Lemma normalise_through_test_forbidden_deroutes : 
-<<<<<<< Updated upstream
       forall e id2 id3 lfb e1 b1 ne ne1,
       Forall (correct_fbd_deroute fp) lfb
       -> full_normalise fp e = ne
@@ -507,16 +506,6 @@ Module FPS_PROP (EVAL_Def: EVAL_ENV)
       -> Common_Sem.test_forbidden_deroutes ne 
               (normalise_block_id fp (get_nav_block e)) id3 lfb
                                               = (b1, ne1).
-=======
-      forall e id2 id3 lfb e1 b1,
-      Forall (correct_fbd_deroute (` (` fps))) lfb
-      -> (normalise_block_id (` (` fps)) id2)
-             = (normalise_block_id (` (` fps)) id3)
-      ->
-      Common_Sem.test_forbidden_deroutes e (get_nav_block e) id2 lfb = (b1, e1) -> 
-      Common_Sem.test_forbidden_deroutes (full_normalise (` (` fps)) e) (normalise_block_id (` (` fps)) (get_nav_block e)) id3 lfb
-       = (b1, (full_normalise (` (` fps)) e1)).
->>>>>>> Stashed changes
     Proof.
       intros e id2 id3 lfb. generalize dependent e. induction lfb.
       - simpl. intros e e1 b1 ne ne1 _ Hne Hne1 _ H1. subst.

tests/error-msg-tests/test3.res

 No SRTM data found to check altitude.
-NOTICE: Deprecated use of 'route' using last waypoint in <go WP="HOME" UNTIL="nav_cond(23)" PRE_CALL="nav_fun(24)" POST_CALL="nav_fun(25)" PITCH="10.5" HMODE="route" ALT="10" no="301"/>
-NOTICE: low altitude (10<185+25) in <go WP="HOME" UNTIL="nav_cond(23)" PRE_CALL="nav_fun(24)" POST_CALL="nav_fun(25)" PITCH="10.5" HMODE="route" ALT="10" no="301"/>
+NOTICE: Deprecated use of 'route' using last waypoint in hmode stage
+NOTICE: low altitude (10<185+25) in convertion vmode alt
 [ERROR] The block 'Test Nav' contains more than 255 stages !

tests/error-msg-tests/test4.res

 No SRTM data found to check altitude.
-NOTICE: Deprecated use of 'route' using last waypoint in <go WP="HOME" UNTIL="nav_cond(23)" PRE_CALL="nav_fun(24)" POST_CALL="nav_fun(25)" PITCH="10.5" HMODE="route" ALT="10" no="301"/>
-NOTICE: low altitude (10<185+25) in <go WP="HOME" UNTIL="nav_cond(23)" PRE_CALL="nav_fun(24)" POST_CALL="nav_fun(25)" PITCH="10.5" HMODE="route" ALT="10" no="301"/>
+NOTICE: Deprecated use of 'route' using last waypoint in hmode stage
+NOTICE: low altitude (10<185+25) in convertion vmode alt
 [ERROR] The block 'Test Nav' contains more than 255 stages !