Ignore:
Timestamp:
Jul 23, 2012, 7:31:11 PM (7 years ago)
Author:
garnier
Message:

Progress on proving semantics preservation under memory injections.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2231 r2234  
    22
    33include "Clight/TypeComparison.ma".
     4include "common/Pointers.ma".
    45
    56lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
     
    2021[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
    2122| 2: #Hneq' normalize // ] qed.
     23
     24lemma eq_block_identity : ∀b. eq_block b b = true. // qed.
Note: See TracChangeset for help on using the changeset viewer.