diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FSetPositive.v | 14 |
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. |