Ignore:
Timestamp:
Jan 9, 2013, 1:23:29 PM (7 years ago)
Author:
garnier
Message:

Progress on toCminorCorrectness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2565 r2572  
    326326(* Useful facts on blocks. *)
    327327(* --------------------------------------------------------------------------- *)
     328
     329lemma eq_block_to_refl : ∀b1,b2. eq_block b1 b2 = true → b1 = b2.
     330#b1 #b2 @(eq_block_elim … b1 b2)
     331[ //
     332| #_ #Habsurd destruct ] qed.
    328333
    329334lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
Note: See TracChangeset for help on using the changeset viewer.