diff options
author | James Pollard <james@pollard.dev> | 2020-06-09 20:29:31 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-09 20:29:31 +0100 |
commit | be89e97e73bb671e2733844521130057b799fca4 (patch) | |
tree | 4d735c12521a19d37dbbe19de20d5962142a06c4 /src/translation/HTLgenproof.v | |
parent | fd84bb3b08fcdfeb40a040ba259e66f421f61f5b (diff) | |
download | vericert-kvx-be89e97e73bb671e2733844521130057b799fca4.tar.gz vericert-kvx-be89e97e73bb671e2733844521130057b799fca4.zip |
Fix automation tactic for modified constructor
Diffstat (limited to 'src/translation/HTLgenproof.v')
-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 *) |