From e9c8da9c2ea50498bcfa7a70c611d5e01a9bd67b Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 9 Jan 2025 16:24:25 -0500 Subject: [PATCH] m --- compiler/src/compiler/FlatImp.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/compiler/src/compiler/FlatImp.v b/compiler/src/compiler/FlatImp.v index 236e51e96..3283a2ed6 100644 --- a/compiler/src/compiler/FlatImp.v +++ b/compiler/src/compiler/FlatImp.v @@ -301,7 +301,7 @@ Module exec. Context {width: Z} {BW: Bitwidth width} {word: word.word width}. Context {mem: map.map word byte} {locals: map.map varname word} {env: map.map String.string (list varname * list varname * stmt varname)}. - Context {ext_spec: ExtSpec} . + Context {ext_spec: ExtSpec}. Context {varname_eq_spec: EqDecider varname_eqb} {word_ok: word.ok word} {mem_ok: map.ok mem} @@ -669,7 +669,6 @@ Module exec. (forall k', pick_sp1 (k' ++ k) = pick_sp2 (k' ++ k)) -> exec (pick_sp := pick_sp2) s k t m l mc post. Proof. - Set Printing Implicit. intros H1 pick_sp2. induction H1; intros; try solve [econstructor; eauto]. - econstructor. 4: eapply exec_extends_trace. all: intuition eauto. { eapply IHexec. intros. rewrite associate_one_left.