From f38fbe6e56bdf69cb5892b5397366ec3d0db9073 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 22 Jun 2020 12:15:53 +0100 Subject: Admit everything temporarily --- src/translation/HTLgenspec.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index b70e11c..887a696 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -370,7 +370,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. @@ -428,8 +428,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. Theorem transl_module_correct : -- cgit