Ignore:
Timestamp:
Jul 6, 2011, 1:29:58 PM (8 years ago)
Author:
campbell
Message:

Evict CompCert? Maps interface in favour of BitVectorTries?.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r961 r1058  
    206206| #v #ty
    207207    whd in ⊢ (???%);
    208     lapply (refl ? (get ident PTree block v en));
    209     cases (get ident PTree block v en) in ⊢ (???% → %);
     208    lapply (refl ? (lookup SymbolTag block en v))
     209    cases (lookup SymbolTag block en v) in ⊢ (???% → %)
    210210    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
    211211        whd; @(eval_Evar_global … eget efind)
Note: See TracChangeset for help on using the changeset viewer.