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 | |
| parent | fd84bb3b08fcdfeb40a040ba259e66f421f61f5b (diff) | |
| download | vericert-kvx-be89e97e73bb671e2733844521130057b799fca4.tar.gz vericert-kvx-be89e97e73bb671e2733844521130057b799fca4.zip | |
Fix automation tactic for modified constructor
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 *) |