diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/translation/HTLgenproof.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index c03f5db..743d369 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -164,7 +164,7 @@ Ltac inv_state := inversion TF; match goal with TC : forall _ _, - Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, H : Maps.PTree.get _ _ = Some _ |- _ => apply TC in H; inversion H; match goal with @@ -298,10 +298,12 @@ Section CORRECTNESS. (* processing of state *) econstructor. simpl. trivial. - econstructor. trivial. + econstructor. + econstructor. econstructor. (* prove stval *) + unfold merge_assocmap. unfold_merge. simpl. apply AssocMap.gss. (* prove match_state *) |