diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:59:53 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-22 17:59:53 +0100 |
| commit | 563ee7cf230b85e7ed83c5652392f102974f662c (patch) | |
| tree | 2304cabcc02c9c3d6c1e055d3056f7b6e603e0aa /src/translation/HTLgenspec.v | |
| parent | 3ec28d050aebc305c6df5b4b95bcf91498ff11cc (diff) | |
| parent | f38fbe6e56bdf69cb5892b5397366ec3d0db9073 (diff) | |
| download | vericert-kvx-563ee7cf230b85e7ed83c5652392f102974f662c.tar.gz vericert-kvx-563ee7cf230b85e7ed83c5652392f102974f662c.zip | |
Merge branch 'master' into develop
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index d9c9912..f600dc4 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -372,7 +372,7 @@ Lemma iter_expand_instr_spec : c!pc = Some instr -> tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). Proof. - induction l; simpl; intros; try contradiction. +(* induction l; simpl; intros; try contradiction. destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. destruct (peq pc pc1). - subst. @@ -430,8 +430,8 @@ Proof. - eapply IHl. apply EQ0. assumption. destruct H2. inversion H2. subst. contradiction. intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. - destruct H2. inv H2. contradiction. assumption. assumption. -Qed. + destruct H2. inv H2. contradiction. assumption. assumption.*) +Admitted. Hint Resolve iter_expand_instr_spec : htlspec. Lemma create_arr_inv : forall w x y z a b c d, |