Changeset 1058 for src/Clight/CexecSound.ma

Timestamp:

Jul 6, 2011, 1:29:58 PM (9 years ago)

Author:

campbell

Message:

Evict CompCert? Maps interface in favour of BitVectorTries?.

File:

• src/Clight/CexecSound.ma (modified) (1 diff)

src/Clight/CexecSound.ma

@@ -206 +206 @@
 | #v #ty
     whd in ⊢ (???%);
-    lapply (refl ? (get ident PTree block v en));
-    cases (get ident PTree block v en) in ⊢ (???% → %);
+    lapply (refl ? (lookup SymbolTag block en v))
+    cases (lookup SymbolTag block en v) in ⊢ (???% → %)
     [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
         whd; @(eval_Evar_global … eget efind)