Cbn is happier when ?SetPositive fixpoints have the set as recursive argument

1 files changed, 7 insertions, 10 deletions

diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index 369672fab..f3a1d39c9 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -111,7 +111,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     | Node l b r => negb b &&& is_empty l &&& is_empty r
    end.
 
-  Fixpoint mem (i : positive) (m : t) : bool :=
+  Fixpoint mem (i : positive) (m : t) {struct m} : bool :=
     match m with
     | Leaf => false
     | Node l o r =>
@@ -148,7 +148,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
        | Leaf,Leaf => Leaf
        | _,_ => Node l false r end.
 
-  Fixpoint remove (i : positive) (m : t) : t :=
+  Fixpoint remove (i : positive) (m : t) {struct m} : t :=
     match m with
       | Leaf => Leaf
       | Node l o r =>
@@ -409,10 +409,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     case o; trivial.
     destruct l; trivial.
     destruct r; trivial.
-    symmetry. destruct x.
-      apply mem_Leaf.
-      apply mem_Leaf.
-      reflexivity.
+    destruct x; reflexivity.
   Qed.
   Local Opaque node.
 
@@ -422,7 +419,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold Empty, In.
     induction s as [|l IHl o r IHr]; simpl.
-      setoid_rewrite mem_Leaf. firstorder.
+      firstorder.
       rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr.
       destruct o; simpl; split.
         intuition discriminate.
@@ -819,7 +816,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold For_all, In. intro f.
     induction s as [|l IHl o r IHr]; intros i; simpl.
-     setoid_rewrite mem_Leaf. intuition discriminate.
+    intuition discriminate.
      rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -844,7 +841,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Proof.
     unfold Exists, In. intro f.
     induction s as [|l IHl o r IHr]; intros i; simpl.
-     setoid_rewrite mem_Leaf. firstorder.
+     firstorder.
      rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
      rewrite IHl, IHr. clear IHl IHr.
       split.
@@ -892,7 +889,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; simpl.
       intros. split; intro H.
         left. assumption.
-        destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_spec Hx').
+        destruct H as [H|[x [Hx Hx']]]. assumption. discriminate.
 
       intros j acc y. case o.
         rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split.