- Timestamp:
- Mar 27, 2013, 9:57:13 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLtoERTLptrOK.ma
r2943 r2991 165 165 definition state_rel ≝ λprog : ertl_program.λf_lbls. 166 166 λf_regs : (block → label → list register). 167 λbl.λ_ :label.λst1,st2.∃f,fn.167 λbl.λ_ : label.λst1,st2.∃f,fn. 168 168 fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧ 169 169 let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in … … 842 842 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); 843 843 >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta 844 >(fetch_stmt_ok_sigma_state_ok … EQfetch) >EQc_bl >m_return_bind 845 lapply EQc_bl' whd in match block_of_call; normalize nodelta 844 846 cases daemon (* CSC: The proof used to be %, why did it change? *) 847 (* This point will be generalized when the call case 848 will be available in StatusSimulationHelper*) 845 849 (* 846 850 XXX
Note: See TracChangeset
for help on using the changeset viewer.