- Timestamp:
- Oct 26, 2011, 5:25:15 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/ProofUtils.ma
r1466 r1467 249 249 let stacksize ≝ joint_if_stacksize … int_fun in 250 250 let code ≝ joint_if_code … int_fun in 251 let entry ≝ ? in 252 let exit ≝ ? in 253 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in 254 let code ≝ relabel_graph params1 sem_params globals state code maps in 255 mk_joint_internal_function … 256 luniverse runiverse result params 257 locals stacksize code entry exit. 251 match joint_if_entry … int_fun with 252 [ dp entry entry_prf ⇒ 253 match joint_if_exit … int_fun with 254 [ dp exit exit_prf ⇒ 255 let 〈maps, code〉 ≝ pre_erase_graph_internal_function params1 sem_params globals state code [ ] in 256 let code ≝ relabel_graph params1 sem_params globals state code maps in 257 mk_joint_internal_function … 258 luniverse runiverse result params 259 locals stacksize code entry exit 260 ] 261 ]. 258 262 cases daemon (* XXX *) 259 263 qed.
Note: See TracChangeset
for help on using the changeset viewer.