Update axiom

src/verification/CommonFPVerification.v

@@ -83,7 +83,7 @@ Section FLIGHT_PLAN.
   Axiom eval_c_code_cond:
     forall code t b,
       EVAL_Def.eval t code = b
-      -> forall ce,  fp_trace_to_trace t = ce.t
+      -> forall ce,  t ~t~ (ce.t)
       -> forall f (f_stmt: expr -> statement) k e le k' e' le' ce'' stmt,
         let ce' := app_ctrace ce [:: cond_event code b] in
         (step2 ge
@@ -115,7 +115,7 @@ Section FLIGHT_PLAN.
 
     rewrite /t -He1' extract_app_trace Heval.
 
-    by apply (eval_c_code_cond Heval (trace_generated_eq He)).
+    by apply (eval_c_code_cond Heval (proj2 He)).
   Qed.
 
   Lemma eval_c_code_ifthenelse:
@@ -212,7 +212,7 @@ Section FLIGHT_PLAN.
       -> forall id ce'' tres ltypes e_p k e le k' e' le' stmt,
           tres = tbool
       -> match_params ltypes e_p params
-      -> forall ce,  fp_trace_to_trace t = ce.t
+      -> forall ce,  t ~t~ (ce.t)
       -> let ce' := app_ctrace ce
           [:: cond_event (gen_fun_call_sem func params) b] in 
           step2 ge
@@ -261,7 +261,7 @@ Section FLIGHT_PLAN.
 
     all: try by exists last.
 
-    all: by apply (trace_generated_eq He).
+    all: by apply (proj2 He).
   Qed.
 
   (** * Lemmas Usefull for the execution of CLight code *)