From e121b1de13ed893a37a73c852e4e9de933eef32a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 10 Jun 2008 18:28:26 +0000
Subject: - Correct handling of DependentMorphism error, using tclFAIL instead
 of   letting the exception go uncatched. - Reorder definitions in Morphisms,
 move the PER on (R ==> R') in   Morphisms where it can be declared properly.
 Add an instance for   Equivalence => Per. - Change bug#1604 test file to the
 new semantics of [setoid_rewrite at] - More unicode characters parsed by
 coqdoc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/1604.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
index 2d0991cb12..22c3df824b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1604.v
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -3,5 +3,5 @@ Require Import Setoid.
 Parameter F : nat -> nat.
 Axiom F_id : forall n : nat, n = F n.
 Goal forall n : nat, F n = n.
-intro n. setoid_rewrite F_id at 2. reflexivity.
+intro n. setoid_rewrite F_id at 3. reflexivity.
 Qed.
-- 
cgit v1.2.3