From a506ee3c2b123decac5508762825e7f2cabff776 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 15 Oct 2009 12:15:07 +0000
Subject: OrderedType2.order is slightly weaker since last commit, adapt
 accordingly

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12392 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/MSets/MSetInterface.v | 6 +++---
 theories/MSets/MSetList.v      | 1 +
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index 630da63028..7b7e23ffa4 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -850,9 +850,9 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
    destruct Disj as [(IN,_)|(IN,_)]; auto. rewrite Hx; auto.
   exists x; split.
   intros z Hz. rewrite (Ad1 z), (Ad2 z).
-  split; intros [U|U]; try order.
-  right; rewrite <- (EQ z); auto.
-  right; rewrite (EQ z); auto.
+  split; intros [U|U]; try (left; order); right.
+  rewrite <- (EQ z); auto.
+  rewrite (EQ z); auto.
   destruct Disj as [(IN,Em)|(IN & y & INy & LTy & Be)].
   left; split; auto.
   rewrite (Ad2 x); auto.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 2b7dbb586f..a6fc0affa7 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -415,6 +415,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
    try sort_inf_in; try order.
+  left; order.
   Qed.
 
   Lemma diff_inf :
-- 
cgit v1.2.3