Changeset 2943

Timestamp:

Mar 23, 2013, 2:07:55 AM (7 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:

• src/ERTL/ERTLtoERTLptrOK.ma (modified) (2 diffs)

src/ERTL/ERTLtoERTLptrOK.ma

@@ -842 +842 @@
        >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
        >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
+       cases daemon (* CSC: The proof used to be %, why did it change? *)
+       (*
+       XXX
        
        [cut (block_of_call
@@ -863 +866 @@
          (sigma_state_pc prog f_lbls f_regs st2))
          
-         [ whd in ⊢ (??%%); normalize nodelta
+         [2: #URCA <URCA cases block_of_call #xyz
+             [2: whd in ⊢ (??%%); %]
+             >m_return_bind >m_return_bind
+             whd in match fetch_internal_function; normalize nodelta
+             whd in match fetch_function; normalize nodelta
          XXX
-         %
+         %*)
   |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
       @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);