Changeset 2943
- Timestamp:
- Mar 23, 2013, 2:07:55 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLtoERTLptrOK.ma
r2942 r2943 842 842 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); 843 843 >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta 844 cases daemon (* CSC: The proof used to be %, why did it change? *) 845 (* 846 XXX 844 847 845 848 [cut (block_of_call … … 863 866 (sigma_state_pc prog f_lbls f_regs st2)) 864 867 865 [ whd in ⊢ (??%%); normalize nodelta 868 [2: #URCA <URCA cases block_of_call #xyz 869 [2: whd in ⊢ (??%%); %] 870 >m_return_bind >m_return_bind 871 whd in match fetch_internal_function; normalize nodelta 872 whd in match fetch_function; normalize nodelta 866 873 XXX 867 % 874 %*) 868 875 |*: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 869 876 @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
Note: See TracChangeset
for help on using the changeset viewer.