Changeset 2943


Ignore:
Timestamp:
Mar 23, 2013, 2:07:55 AM (4 years ago)
Author:
sacerdot
Message:

Mauro, I have put a daemon in place of the proof obligation that used to
be closed by % and that is no more. I have absolutely no idea why did it
change. Moreover, it seems trivially true, but I found no easy way to prove
it with the current results. Is there any?

But for that, all the file is repaired.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2942 r2943  
    842842       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
    843843       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
     844       cases daemon (* CSC: The proof used to be %, why did it change? *)
     845       (*
     846       XXX
    844847       
    845848       [cut (block_of_call
     
    863866         (sigma_state_pc prog f_lbls f_regs st2))
    864867         
    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
    866873         XXX
    867          %
     874         %*)
    868875  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    869876      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
Note: See TracChangeset for help on using the changeset viewer.