From 7e52301b501f7a574fca19776fb7fcbfe873d533 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 30 Mar 2010 21:26:06 +0000 Subject: Small things about coqdoc + fixing lettuple.v test (part of bug #2289) In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/complexity/lettuple.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/complexity') diff --git a/test-suite/complexity/lettuple.v b/test-suite/complexity/lettuple.v index f97decf0a..0690459fc 100644 --- a/test-suite/complexity/lettuple.v +++ b/test-suite/complexity/lettuple.v @@ -26,4 +26,4 @@ Definition f (x : nat * nat) := let (a,b) := x in 0. -Timeout 5 Print f. +Timeout 5 Time Print f. -- cgit v1.2.3