Changeset 1058 for src/Clight/CexecSound.ma
- Timestamp:
- Jul 6, 2011, 1:29:58 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecSound.ma
r961 r1058 206 206 | #v #ty 207 207 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 ⊢ (???% → %) 210 210 [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind 211 211 whd; @(eval_Evar_global … eget efind)
Note: See TracChangeset
for help on using the changeset viewer.