From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 19 Jul 2019 18:59:44 +0200
Subject: helpers broke compilation

---
 x86/SelectOp.vp     | 7 +------
 x86/SelectOpproof.v | 5 +----
 2 files changed, 2 insertions(+), 10 deletions(-)

(limited to 'x86')

diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index d734ecc6..a23c37d5 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,11 +40,8 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
-<<<<<<< HEAD
 Require Import OpHelpers.
-=======
 Require Archi.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 
 Local Open Scope cminorsel_scope.
 
@@ -580,16 +577,14 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
-<<<<<<< HEAD
 (* floats *)
 Definition divf_base (e1: expr) (e2: expr) :=
   Eop Odivf (e1 ::: e2 ::: Enil).
 
 Definition divfs_base (e1: expr) (e2: expr) :=
   Eop Odivfs (e1 ::: e2 ::: Enil).
-=======
+
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
   None.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index b59f4a87..5703c758 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -1016,8 +1016,6 @@ Proof.
 - constructor; auto.
 Qed.
 
-<<<<<<< HEAD
-
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
   forall le a b x y,
@@ -1038,7 +1036,7 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
-=======
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin:
@@ -1051,5 +1049,4 @@ Proof.
   intros. discriminate.
 Qed.
 
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 End CMCONSTR.
-- 
cgit