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/SelectOp.vp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'riscV/SelectOp.vp')

diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 23235d95..e9920e46 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -452,16 +452,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
-- 
cgit