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

---
 riscV/SelectOpproof.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'riscV/SelectOpproof.v')

diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index ca271342..52a535fb 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -933,8 +933,6 @@ Proof.
 - constructor; auto.
 Qed.
 
-<<<<<<< HEAD
-
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
   forall le a b x y,
@@ -955,7 +953,7 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
-=======
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin:
@@ -968,5 +966,4 @@ Proof.
   intros. discriminate.
 Qed.
 
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 End CMCONSTR.
-- 
cgit