From 8dfcf43a839b2e893818b67702a3ee305971a624 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Sun, 4 May 2014 11:08:39 +0200
Subject: Fix after merge.

---
 theories/FSets/FSetPositive.v | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'theories/FSets')

diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index efd49f54e..88011ff1c 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -45,11 +45,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     | Node l b r => negb b &&& is_empty l &&& is_empty r
    end.
 
-<<<<<<< HEAD
-  Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
-=======
-  Fixpoint mem (i : elt) (m : t) : bool :=
->>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
+  Fixpoint mem (i : elt) (m : t) {struct m} : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -86,11 +82,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        | Leaf,Leaf => Leaf
        | _,_ => Node l false r end.
 
-<<<<<<< HEAD
-  Fixpoint remove (i : positive) (m : t) {struct m} : t :=
-=======
-  Fixpoint remove (i : elt) (m : t) : t :=
->>>>>>> This commit adds full universe polymorphism and fast projections to Coq.
+  Fixpoint remove (i : elt) (m : t) {struct m} : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -358,7 +350,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     case o; trivial.
     destruct l; trivial.
     destruct r; trivial.
-  now destruct x.
+    now destruct x.
   Qed.
   Local Opaque node.
 
-- 
cgit v1.2.3