Changeset 2722 for src/Clight/switchRemoval.ma
- Timestamp:
- Feb 23, 2013, 5:05:03 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/switchRemoval.ma
r2706 r2722 1923 1923 rg_find_symbol: ∀s. 1924 1924 find_symbol ? ge s = find_symbol ? ge' s; 1925 rg_find_funct : ∀v,f.1926 find_funct ? ge v = Some ? f→1927 find_funct ? ge' v = Some ? (t f);1925 rg_find_funct_id: ∀v,f,id. 1926 find_funct_id ? ge v = Some ? 〈f,id〉 → 1927 find_funct_id ? ge' v = Some ? 〈t f,id〉; 1928 1928 rg_find_funct_ptr: ∀b,f. 1929 1929 find_funct_ptr ? ge b = Some ? f → … … 2913 2913 cases (bindIO_inversion ??????? Hexec) #xfunc * #Heq_func #Hexec_func 2914 2914 cases (bindIO_inversion ??????? Hexec_func) #xargs * #Heq_args #Hexec_args 2915 cases (bindIO_inversion ??????? Hexec_args) #called_fundef* #Heq_fundef #Hexec_typeeq2915 cases (bindIO_inversion ??????? Hexec_args) * #called_fundef #fid * #Heq_fundef #Hexec_typeeq 2916 2916 cases (bindIO_inversion ??????? Hexec_typeeq) #Htype_eq * #Heq_assert #Hexec_ret 2917 2917 >(Hsim_expr … Heq_func) whd in match (m_bind ?????); 2918 2918 >(exec_expr_sim_to_exec_exprlist … Hsim_expr … Heq_args) 2919 2919 whd in ⊢ (??%?); 2920 >(rg_find_funct … Hrelated … (opt_to_io_Value … Heq_fundef))2920 >(rg_find_funct_id … Hrelated … (opt_to_io_Value … Heq_fundef)) 2921 2921 whd in ⊢ (??%?); <fundef_type_simplify >Heq_assert 2922 2922 whd in ⊢ (??%?); -Hexec -Hexec_func -Hexec_args -Hexec_typeeq lapply Hexec_ret -Hexec_ret
Note: See TracChangeset
for help on using the changeset viewer.