From f6007680bfa822ecc3d2f101fb6e21e2b1464b1b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 1 Jul 2008 17:03:43 +0000
Subject: Various bug fixes in type classes and subtac: - Cases on multiple
 objects - Avoid dangerous coercion with evars in subtac_coercion - Resolve
 typeclasses method-by-method to get better error messages. - Correct merging
 of instance databases (and add debug printer) - Fix a script in NOrder where
 a setoid_replace was not working before.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11198 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Natural/Abstract/NOrder.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index bcd4b92d6c..5212e63814 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -309,13 +309,12 @@ Proof NZgt_wf.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)).
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) 
+  using relation (@relations_eq N N).
+apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
-rewrite H; apply lt_wf.
-(* does not work:
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
-Qed.
+Defined.
 
 (* Theorems that are true for natural numbers but not for integers *)
 
-- 
cgit v1.2.3