From bb95ebda330d59474bd0793a8d4e0f51face118f Mon Sep 17 00:00:00 2001
From: coq
Date: Mon, 5 May 2003 13:35:31 +0000
Subject: Corrige Bug (PR#290)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3989 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/modules/PO.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index aafbbf2a1a..b16ab28096 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -15,7 +15,7 @@ Module Type PO.
 End PO.
 
 
-Module Pair[X:PO][Y:PO].
+Module Pair[X:PO][Y:PO]<:PO.
   Definition T:=X.T*Y.T.
   Definition le:=[p1,p2]
     (X.le (fst p1) (fst p2)) /\ (Y.le (snd p1) (snd p2)).
@@ -23,12 +23,12 @@ Module Pair[X:PO][Y:PO].
   Hints Unfold le.
 
   Lemma le_refl : (p:T)(le p p).
-  Auto.
+  Info Auto.
   Save.
 
   Lemma le_trans : (p1,p2,p3:T)(le p1 p2) -> (le p2 p3) -> (le p1 p3).
     Unfold le.
-    Intuition; EAuto.
+    Intuition; Info EAuto.
   Save.    
 
   Lemma le_antis : (p1,p2:T)(le p1 p2) -> (le p2 p1) -> (p1=p2).
@@ -60,7 +60,6 @@ Module Type Fmono.
   Axiom f_mono : (x1,x2:X.T)(X.le x1 x2) -> (Y.le (f x1) (f x2)).
 End Fmono.
 
-
 Read Module Nat.
 
 
-- 
cgit v1.2.3