fix riscv merge?

5 files changed, 0 insertions, 488 deletions

diff --git a/riscV/TO_MERGE/Asm.v b/riscV/Asm.v
index f75825a1..7e8ba760 100644
--- a/riscV/TO_MERGE/Asm.v
+++ b/riscV/Asm.v
@@ -256,17 +256,10 @@ Inductive instruction : Type :=
 
   (* floating point register move *)
   | Pfmv     (rd: freg) (rs: freg)                  (**r move *)
-<<<<<<< HEAD
   | Pfmvxs   (rd: ireg) (rs: freg)                  (**r bitwise move FP single to integer register *)
   | Pfmvxd   (rd: ireg) (rs: freg)                  (**r bitwise move FP double to integer register *)
   | Pfmvsx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP single *)
   | Pfmvdx   (rd: freg) (rs: ireg)                  (**r bitwise move integer register to FP double*)
-=======
-  | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
-  | Pfmvsx   (rd: freg) (rs: ireg)                  (**r move integer register to FP single *)
-  | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
-  | Pfmvdx   (rd: freg) (rs: ireg)                  (**r move integer register to FP double *)
->>>>>>> master
 
   (* 32-bit (single-precision) floating point *)
   | Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
@@ -994,14 +987,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       so we do not model them. *)
   | Pfence
 
-<<<<<<< HEAD
-=======
-  | Pfmvxs _ _
-  | Pfmvsx _ _
-  | Pfmvxd _ _
-  | Pfmvdx _ _
-
->>>>>>> master
   | Pfmins _ _ _
   | Pfmaxs _ _ _
   | Pfsqrts _ _
diff --git a/riscV/TO_MERGE/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 1a8ce27d..379b5789 100644
--- a/riscV/TO_MERGE/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -432,408 +432,6 @@ Proof.
   intros; Simpl. 
 Qed.
 
-<<<<<<< HEAD
-=======
-(** Translation of condition operators *)
-
-Lemma transl_cond_int32s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool.
-  simpl. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). 
-  destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int32u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool.
-  simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64s_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool.
-  simpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). 
-  destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_cond_int64u_correct:
-  forall cmp rd r1 r2 k rs m,
-  exists rs',
-     exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m
-  /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2)
-  /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. 
-Proof.
-  intros. destruct cmp; simpl. 
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool.
-  simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto.
-- econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto.
-- econstructor; split.
-  eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. 
-  split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). 
-  destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto.
-Qed.
-
-Lemma transl_condimm_int32s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32s.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm32. 
-  exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int.lt. rewrite zlt_false. auto. 
-  change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed.
-  generalize (Int.signed_range i); lia.
-* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1).
-  destruct (zlt (Int.signed n) (Int.signed i)).
-  rewrite zlt_false by lia. auto.
-  rewrite zlt_true by lia. auto.
-  rewrite Int.add_signed. symmetry; apply Int.signed_repr. 
-  assert (Int.signed n <> Int.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. }
-  generalize (Int.signed_range n); lia.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int32u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int32u.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64s_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64s.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C).
-  exists rs'; eauto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ unfold xorimm64. 
-  exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1).
-  exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2).
-  exists rs2; split. 
-  eapply exec_straight_trans. eexact A1. eexact A2. 
-  split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto.
-  unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2.
-  intros; transitivity (rs1 r); auto.
-+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed).
-* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. 
-  unfold Int64.lt. rewrite zlt_false. auto. 
-  change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed.
-  generalize (Int64.signed_range i); lia.
-* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. 
-  rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto.
-  unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1).
-  destruct (zlt (Int64.signed n) (Int64.signed i)).
-  rewrite zlt_false by lia. auto.
-  rewrite zlt_true by lia. auto.
-  rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. 
-  assert (Int64.signed n <> Int64.max_signed).
-  { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. }
-  generalize (Int64.signed_range n); lia.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_condimm_int64u_correct:
-  forall cmp rd r1 n k rs m,
-  r1 <> X31 ->
-  exists rs',
-     exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m
-  /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  intros. unfold transl_condimm_int64u.
-  predSpec Int64.eq Int64.eq_spec n Int64.zero.
-- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C).
-  exists rs'; split. eexact A. split; auto. rewrite B; auto.
-- assert (DFL:
-    exists rs',
-      exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m
-   /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd
-   /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r).
-  { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1).
-    exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2).
-    exists rs2; split. 
-    eapply exec_straight_trans. eexact A1. eexact A2. 
-    split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto.
-    intros; transitivity (rs1 r); auto. }
-  destruct cmp.
-+ apply DFL.
-+ apply DFL.
-+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto.
-  intros (rs1 & A1 & B1 & C1).
-  exists rs1; split. eexact A1. split; auto. rewrite B1; auto.
-+ apply DFL.
-+ apply DFL.
-+ apply DFL.
-Qed.
-
-Lemma transl_cond_op_correct:
-  forall cond rd args k c rs m,
-  transl_cond_op cond rd args k = OK c ->
-  exists rs',
-     exec_straight ge fn c rs m k rs' m
-  /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd
-  /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r.
-Proof.
-  assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)).
-  { destruct ob as [[]|]; reflexivity. }
-  intros until m; intros TR.
-  destruct cond; simpl in TR; ArgsInv.
-+ (* cmp *)
-  exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto.
-+ (* cmpu *)
-  exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B; auto.
-+ (* cmpimm *)
-  apply transl_condimm_int32s_correct; eauto with asmgen.
-+ (* cmpuimm *)
-  apply transl_condimm_int32u_correct; eauto with asmgen.
-+ (* cmpl *)
-  exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmplu *)
-  exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto.
-+ (* cmplimm *)
-  exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpluimm *)
-  exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. 
-  intros (rs' & A & B & C).
-  exists rs'; repeat split; eauto. rewrite MKTOT; eauto.
-+ (* cmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpf *)
-  destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)).
-  set (v := Val.cmpf c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_float_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-+ (* cmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto.
-  split; intros; Simpl.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := Val.notbool v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-+ (* notcmpfs *)
-  destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR.
-  rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)).
-  set (v := Val.cmpfs c0 (rs x) (rs x0)).
-  destruct normal; inv EQ2.
-* econstructor; split.
-  eapply exec_straight_two.
-  eapply transl_cond_single_correct with (v := v); eauto.
-  simpl; reflexivity.
-  auto. auto.
-  split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto.
-* econstructor; split.
-  apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto.
-  split; intros; Simpl.
-Qed.
-
->>>>>>> master
 (** Some arithmetic properties. *)
 
 Remark cast32unsigned_from_cast32signed:
diff --git a/riscV/TO_MERGE/SelectLongproof.v b/riscV/SelectLongproof.v
index 954dd134..0fc578bf 100644
--- a/riscV/TO_MERGE/SelectLongproof.v
+++ b/riscV/SelectLongproof.v
@@ -506,39 +506,9 @@ Proof.
 - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto.
   change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto.
 - TrivialExists.
-<<<<<<< HEAD
   cbn.
   rewrite H0.
   reflexivity.
-=======
-(*
-  intros. unfold shrxlimm. destruct Archi.splitlong eqn:SL.
-+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32.
-+ destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 63)) eqn:LTU; inv H0.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vlong i); split; auto. rewrite Int64.shrx'_zero. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 63) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int64.iwordsize' n) Int64.iwordsize' = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int64.iwordsize') with 64. 
-      rewrite Int.unsigned_repr. lia. 
-      assert (64 < Int.max_unsigned) by reflexivity. lia. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrlimm (Int.repr (Int64.zwordsize - 1))) (a ::: Enil))
-               (Vlong (Int64.shr' i (Int.repr (Int64.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrxlimm_inner a n)
-               (Vlong (Int64.shru' (Int64.shr' i (Int.repr (Int64.zwordsize - 1))) (Int.sub Int64.iwordsize' n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int64.shrx'_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int64.iwordsize') with 64; lia.
-*)
->>>>>>> master
 Qed.
 
 Theorem eval_cmplu:
diff --git a/riscV/TO_MERGE/SelectOpproof.v b/riscV/SelectOpproof.v
index 9bd66213..f450fe6c 100644
--- a/riscV/TO_MERGE/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -574,43 +574,12 @@ Proof.
   replace (Int.shrx i Int.zero) with i. auto.
   unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
   change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
-<<<<<<< HEAD
   econstructor; split. EvalOp.
   cbn.
   rewrite H0.
   cbn.
   reflexivity.
   apply Val.lessdef_refl.
-=======
-  econstructor; split. EvalOp. auto.
-(*
-  intros. destruct x; simpl in H0; try discriminate. 
-  destruct (Int.ltu n (Int.repr 31)) eqn:LTU; inv H0.
-  unfold shrximm.
-  predSpec Int.eq Int.eq_spec n Int.zero.
-  - subst n. exists (Vint i); split; auto.
-    unfold Int.shrx, Int.divs. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto.
-  - assert (NZ: Int.unsigned n <> 0).
-    { intro EQ; elim H0. rewrite <- (Int.repr_unsigned n). rewrite EQ; auto. }
-    assert (LT: 0 <= Int.unsigned n < 31) by (apply Int.ltu_inv in LTU; assumption).
-    assert (LTU2: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true).
-    { unfold Int.ltu; apply zlt_true.
-      unfold Int.sub. change (Int.unsigned Int.iwordsize) with 32. 
-      rewrite Int.unsigned_repr. lia. 
-      assert (32 < Int.max_unsigned) by reflexivity. lia. }
-    assert (X: eval_expr ge sp e m le
-               (Eop (Oshrimm (Int.repr (Int.zwordsize - 1))) (a ::: Enil))
-               (Vint (Int.shr i (Int.repr (Int.zwordsize - 1))))).
-    { EvalOp. }
-    assert (Y: eval_expr ge sp e m le (shrximm_inner a n)
-               (Vint (Int.shru (Int.shr i (Int.repr (Int.zwordsize - 1))) (Int.sub Int.iwordsize n)))).
-    { EvalOp. simpl. rewrite LTU2. auto. }
-    TrivialExists. 
-    constructor. EvalOp. simpl; eauto. constructor. 
-    simpl. unfold Int.ltu; rewrite zlt_true. rewrite Int.shrx_shr_2 by auto. reflexivity. 
-    change (Int.unsigned Int.iwordsize) with 32; lia.
-*)
->>>>>>> master
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
diff --git a/riscV/TO_MERGE/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 23fbeb8b..aab6b9b8 100644
--- a/riscV/TO_MERGE/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -107,15 +107,10 @@ module Target : TARGET =
 
     let name_of_section = function
       | Section_text         -> ".text"
-<<<<<<< HEAD
       | Section_data(i, true) ->
          failwith "_Thread_local unsupported on this platform"
       | Section_data(i, false) | Section_small_data i ->
-          if i then ".data" else common_section ()
-=======
-      | Section_data i | Section_small_data i ->
           variable_section ~sec:".data" ~bss:".bss" i
->>>>>>> master
       | Section_const i | Section_small_const i ->
           variable_section ~sec:".section	.rodata" i
       | Section_string       -> ".section	.rodata"
@@ -403,11 +398,6 @@ module Target : TARGET =
          fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
       | Pfmvxd (rd,fs) ->
          fprintf oc "	fmv.x.d	%a, %a\n"     ireg rd freg fs
-<<<<<<< HEAD
-      | Pfmvsx (fd,rs) ->
-         fprintf oc "	fmv.s.x	%a, %a\n"     freg fd ireg rs
-=======
->>>>>>> master
       | Pfmvdx (fd,rs) ->
          fprintf oc "	fmv.d.x	%a, %a\n"     freg fd ireg rs