Fix after merge.

1 files changed, 3 insertions, 11 deletions

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.