Skip to content
Snippets Groups Projects
Commit 17e47394 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update notation

parent 3e9c8046
No related branches found
No related tags found
No related merge requests found
......@@ -206,7 +206,7 @@ Section FLIGHT_PLAN.
can be converted into a trace and replaced by a boolean constant.
This constant is the result of the evaluation of the condition using
evalc function.*)
Axiom exec_arbitrary_fun_call_with_res:
Axiom exec_arb_call_with_res:
forall f func params t b,
EVAL_Def.eval t (gen_fun_call_sem func params) = b
-> forall id m' tres ltypes e_p k e le k' e' le' stmt,
......@@ -256,7 +256,7 @@ Section FLIGHT_PLAN.
all: rewrite /t -He1' extract_app_trace Heval.
all: apply (exec_arbitrary_fun_call_with_res Heval);
all: apply (exec_arb_call_with_res Heval);
try by []; simpl_eqparam_ex wp.
all: try by exists last.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment