From be89e97e73bb671e2733844521130057b799fca4 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Tue, 9 Jun 2020 20:29:31 +0100 Subject: Fix automation tactic for modified constructor --- src/translation/HTLgenproof.v | 6 ++++-- 1 file 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 *) -- cgit