Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSets, and improve it

 As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt)))
 and a few basic properties over them, you can instantiate functor MakeOrderTac
 and gain an "order" tactic. See comments in the file for the scope of this tactic.

 NB: order doesn't call auto anymore. It only searches for a contradiction in the
 current set of (in)equalities (after the goal was optionally turned into hyp
 by double negation). Thanks to S. Lescuyer for his suggestions about this tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12397 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 3 insertions, 3 deletions

diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index d5cbea61c..119868f4e 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -865,12 +865,12 @@ Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
   destruct Disj as [(IN,Em)|(IN & y & INy & LTy & Be)].
   left; split; auto.
   rewrite (Ad2 x); auto.
-  intros z. rewrite (Ad1 z); intros [U|U]; try specialize (Ab1 z U); order.
+  intros z. rewrite (Ad1 z); intros [U|U]; try specialize (Ab1 z U); auto; order.
   right; split; auto.
   rewrite (Ad1 x); auto.
   exists y; repeat split; auto.
   rewrite (Ad2 y); auto.
-  intros z. rewrite (Ad2 z). intros [U|U]; try specialize (Ab2 z U); order.
+  intros z. rewrite (Ad2 z). intros [U|U]; try specialize (Ab2 z U); auto; order.
   Qed.
 
 End MakeSetOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index a6fc0affa..471b43e24 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -442,7 +442,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
    try sort_inf_in; try order.
-  right; intuition; inv; order.
+  right; intuition; inv; auto.
   Qed.
 
   Lemma equal_spec :