Changeset 2677 for src/Clight/switchRemoval.ma
- Timestamp:
- Feb 19, 2013, 12:23:50 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2608 r2677 1987 1987 (State sss_func_tr sss_result sss_k_ext sss_env_ext sss_m_ext) 1988 1988 | sws_callstate : 1989 ∀ssc_vf. 1989 1990 ∀ssc_fd. 1990 1991 ∀ssc_args. … … 1999 2000 switch_cont_sim (\snd (function_switch_removal ssc_f)) ssc_k ssc_k_ext 2000 2001 | _ ⇒ True ]) → 2001 switch_state_sim ge (Callstate ssc_ fd ssc_args ssc_k ssc_m)2002 (Callstate (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext)2002 switch_state_sim ge (Callstate ssc_vf ssc_fd ssc_args ssc_k ssc_m) 2003 (Callstate ssc_vf (fundef_switch_removal ssc_fd) ssc_args ssc_k_ext ssc_m_ext) 2003 2004 | sws_returnstate : 2004 2005 ∀ssr_result.
Note: See TracChangeset
for help on using the changeset viewer.