Cleanup

1 files changed, 28 insertions, 28 deletions

diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v
index a47654b8..4217f526 100644
--- a/aarch64/Asmblockgenproof0.v
+++ b/aarch64/Asmblockgenproof0.v
@@ -200,9 +200,9 @@ Lemma agree_set_pair:
   agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs).
 Proof.
   intros. destruct p; simpl.
-- apply agree_set_mreg_parallel; auto.
-- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
-  apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
+  - apply agree_set_mreg_parallel; auto.
+  - apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto.
+    apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto.
 Qed.
 
 Lemma agree_set_res:
@@ -212,12 +212,12 @@ Lemma agree_set_res:
   agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs).
 Proof.
   induction res; simpl; intros.
-- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
-  intros. apply Pregmap.gso; auto.
-- auto.
-- apply IHres2. apply IHres1. auto.
-  apply Val.hiword_lessdef; auto.
-  apply Val.loword_lessdef; auto.
+  - eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto.
+    intros. apply Pregmap.gso; auto.
+  - auto.
+  - apply IHres2. apply IHres1. auto.
+    apply Val.hiword_lessdef; auto.
+    apply Val.loword_lessdef; auto.
 Qed.
 
 Lemma agree_undef_regs:
@@ -257,15 +257,15 @@ Lemma agree_undef_caller_save_regs:
   agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
 Proof.
   intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split.
-- unfold proj_sumbool; rewrite dec_eq_true. auto.
-- auto.
-- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
-  destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
-+ apply list_in_map_inv in i. destruct i as (mr & A & B). 
-  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
-  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
-+ destruct (is_callee_save r) eqn:CS; auto.
-  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+  - unfold proj_sumbool; rewrite dec_eq_true. auto.
+  - auto.
+  - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+    destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
+    + apply list_in_map_inv in i. destruct i as (mr & A & B). 
+      assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+      apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
+    + destruct (is_callee_save r) eqn:CS; auto.
+      elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
 Qed.
 
 Lemma agree_change_sp:
@@ -327,10 +327,10 @@ Lemma extcall_arg_pair_match:
   exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'.
 Proof.
   intros. inv H1.
-- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
-- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
-  exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
-  exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
+  - exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto.
+  - exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1).
+    exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2).
+    exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto.
 Qed.
 
 Lemma extcall_args_match:
@@ -362,9 +362,9 @@ Lemma set_res_other:
   set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r.
 Proof.
   induction res; simpl; intros.
-- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate.
-- auto.
-- rewrite IHres2, IHres1; auto.
+  - apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate.
+  - auto.
+  - rewrite IHres2, IHres1; auto.
 Qed.
 
 Lemma undef_regs_other:
@@ -720,8 +720,8 @@ Lemma exec_straight_opt_step:
   exec_straight (i :: c) rs1 m1 c' rs3 m3.
 Proof.
   intros. inv H0.
-- apply exec_straight_one; auto.
-- eapply exec_straight_step; eauto.
+  - apply exec_straight_one; auto.
+  - eapply exec_straight_step; eauto.
 Qed.
 
 Lemma exec_straight_opt_step_opt:
@@ -882,4 +882,4 @@ Proof.
   intros. inv H0. auto. exploit parent_ra_def; eauto. tauto.
 Qed.
 
-End MATCH_STACK.
\ No newline at end of file
+End MATCH_STACK.