From ec850ff623801e514b3ed0a42beb6f7984992520 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Mar 2008 16:32:12 +0000
Subject: Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As
 part of the fix I added an optional "by" annotation for rewrite to solve said
 conditions in the same tactic call. Most of the theories have been updated,
 only FSets is missing, Pierre will take care of it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/NArith/BinPos.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/NArith')

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 36a8458241..f0751f670a 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -802,7 +802,7 @@ Qed.
 Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
 Proof.
   intro x; induction x as [p IHp| p IHp| ]; intro y; destruct y as [q| q| ];
-    simpl in |- *; auto; intro H;
+    simpl in |- *; auto; intro H ;
       [ rewrite (IHp q); trivial
         | absurd ((p ?= q) Gt = Eq);
           [ elim (Pcompare_not_Eq p q); auto | assumption ]
-- 
cgit v1.2.3