diff options
Diffstat (limited to 'kvx/lib/Machblock.v')
| -rw-r--r-- | kvx/lib/Machblock.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kvx/lib/Machblock.v b/kvx/lib/Machblock.v index edae0ed4..404c2a96 100644 --- a/kvx/lib/Machblock.v +++ b/kvx/lib/Machblock.v @@ -70,7 +70,7 @@ Lemma bblock_eq: b1 = b2. Proof. intros. destruct b1. destruct b2. - simpl in *. subst. auto. + cbn in *. subst. auto. Qed. Definition length_opt {A} (o: option A) : nat := @@ -85,15 +85,15 @@ Lemma size_null b: size b = 0%nat -> header b = nil /\ body b = nil /\ exit b = None. Proof. - destruct b as [h b e]. simpl. unfold size. simpl. + destruct b as [h b e]. cbn. unfold size. cbn. intros H. assert (length h = 0%nat) as Hh; [ omega |]. assert (length b = 0%nat) as Hb; [ omega |]. assert (length_opt e = 0%nat) as He; [ omega|]. repeat split. - destruct h; try (simpl in Hh; discriminate); auto. - destruct b; try (simpl in Hb; discriminate); auto. - destruct e; try (simpl in He; discriminate); auto. + destruct h; try (cbn in Hh; discriminate); auto. + destruct b; try (cbn in Hb; discriminate); auto. + destruct e; try (cbn in He; discriminate); auto. Qed. (** ** programs *) @@ -127,13 +127,13 @@ Definition is_label (lbl: label) (bb: bblock) : bool := Lemma is_label_correct_true lbl bb: List.In lbl (header bb) <-> is_label lbl bb = true. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. Lemma is_label_correct_false lbl bb: ~(List.In lbl (header bb)) <-> is_label lbl bb = false. Proof. - unfold is_label; destruct (in_dec lbl (header bb)); simpl; intuition. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. Qed. |