Update notations

src/verification/MatchFPSwFPC.v

@@ -120,8 +120,8 @@ Module MATCH_FPS_C (EVAL_Def: EVAL_ENV)
     (** Match properties about fp_env and a memory state. Every
         flight plan information of the fp_env (for example nav_stage or
         nav_block) must be stored somewhere in the memory. *)
-    Record match_env (ge: genv) (e: fp_env) (e': m_env)
-                            := create_match_env {
+    Record match_menv (ge: genv) (e: fp_env) (e': m_env)
+                            := create_match_menv {
       correct_nav_block: correct_mem_access ge e'
                                   CommonFP._nav_block
                                 (create_val (get_nav_block e));
@@ -152,18 +152,18 @@ Module MATCH_FPS_C (EVAL_Def: EVAL_ENV)
 
   (** An fp_env and a c_env are matching iff the memory state is
       matching to the fp_env and they have matching memory states. *)
-  Definition match_fp_cenv (ge: genv) (e: fp_env8) (e': fp_cenv): Prop :=
-    match_env ge (` e) (get_m_env e')
+  Definition match_env (ge: genv) (e: fp_env8) (e': fp_cenv): Prop :=
+    match_menv ge (` e) (get_m_env e')
     /\ (get_trace (` e)) ~t~ (C_ENV.get_trace e').
 
   End MATCH_ENV.
   Import MATCH_ENV.
 
   Notation "e1 '~menv~' '(' ge ',' e2 ')'"
-    := (match_env ge e1 e2) (at level 10).
+    := (match_menv ge e1 e2) (at level 10).
 
   Notation "e1 '~cenv~' '(' p ',' e2 ')'"
-    := (match_fp_cenv p e1 e2) (at level 10).
+    := (match_env p e1 e2) (at level 10).
 
   (** ** Proporties about the matching relation *)
   Lemma app_trace_preserve_mmatch:

src/verification/VerifFPSToFPC.v

@@ -956,7 +956,7 @@ Section FLIGHT_PLAN.
                               (extract_evalc Hevalc)
                               (extract_evalc Hevalc')) app_assoc.
 
-              rewrite /MATCH_ENV.match_fp_cenv -He1'_f Heqe1'''.
+              rewrite /MATCH_ENV.match_env -He1'_f Heqe1'''.
               by apply app_trace_preserve_match2. }
 
            (* Until condition evaluated to false *)
@@ -1074,7 +1074,7 @@ Section FLIGHT_PLAN.
             (trace_appended_app_trace_rec _ (extract_next_stage (` e1'))).
 
         all: rewrite Heqe1'' in Heq.
-        all: rewrite /MATCH_ENV.match_fp_cenv -Heq.
+        all: rewrite /MATCH_ENV.match_env -Heq.
         all: by apply app_trace_preserve_match2. }
      }
 
@@ -1115,7 +1115,7 @@ Section FLIGHT_PLAN.
                 -extract_trace_next_stage
                 extract_trace_refl extract_app_trace //.
 
-      all: rewrite /MATCH_ENV.match_fp_cenv -Heq Heqe1'.
+      all: rewrite /MATCH_ENV.match_env -Heq Heqe1'.
 
       all: by apply app_trace_preserve_match2.
 
@@ -1824,7 +1824,7 @@ Section FLIGHT_PLAN.
               (State f Sskip  (block_cont_e (` e1) k) ev le' (e2'.m))))
                 /\ e1' ~cenv~ (ge, e2').
   Proof.
-    rewrite /MATCH_ENV.match_fp_cenv.
+    rewrite /MATCH_ENV.match_env.
     move => E1 E1' e2 le H H'.
     generalize dependent e2. generalize dependent le.
     have H := (run_step_ind8 fps P_eq_exec_stages _ _ E1 E1' H').
@@ -2989,7 +2989,7 @@ Section FLIGHT_PLAN.
                             (C_BS.semantics_fpc prog).
   Proof.
     apply FPBigStepGeneric.Bisimulation
-      with (@MATCH_ENV.match_fp_cenv ge); do 2 split.
+      with (@MATCH_ENV.match_env ge); do 2 split.
     - move => e1 H.
       destruct (semantics_init_exists fps gvars) as [e_init Hinit].
       exists e_init; split; try by [].