OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with Inline)

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

2 files changed, 4 insertions, 10 deletions

diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v
index 08391d33f..06db5fa1c 100644
--- a/theories/NArith/NOrderedType.v
+++ b/theories/NArith/NOrderedType.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinNat
- DecidableType2 OrderedType2 OrderedType2Facts.
+Require Import BinNat DecidableType2 OrderedType2 OrderTac.
 
 Local Open Scope N_scope.
 
@@ -54,9 +53,7 @@ End N_as_OT.
 (** * An [order] tactic for [N] numbers *)
 
 Module NOrder := OTF_to_OrderTac N_as_OT.
-Ltac n_order :=
- change (@eq N) with NOrder.OrderElts.eq in *;
- NOrder.order.
+Ltac n_order := NOrder.order.
 
 (** Note that [n_order] is domain-agnostic: it will not prove
     [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v
index 85667e29a..041a3a01b 100644
--- a/theories/NArith/POrderedType.v
+++ b/theories/NArith/POrderedType.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import BinPos
- DecidableType2 OrderedType2 OrderedType2Facts.
+Require Import BinPos DecidableType2 OrderedType2 OrderTac.
 
 Local Open Scope positive_scope.
 
@@ -55,9 +54,7 @@ End Positive_as_OT.
 (** * An [order] tactic for positive numbers *)
 
 Module PositiveOrder := OTF_to_OrderTac Positive_as_OT.
-Ltac p_order :=
- change (@eq positive) with PositiveOrder.OrderElts.eq in *;
- PositiveOrder.order.
+Ltac p_order := PositiveOrder.order.
 
 (** Note that [p_order] is domain-agnostic: it will not prove
     [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)