From 3e618e464acfd001feed85795783108c5aa76a55 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 17 Dec 2011 15:38:36 +0000 Subject: Fixing format of complexity bug Notations.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/complexity/Notations.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/complexity') diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v index d36d77d57..02a3c2528 100644 --- a/test-suite/complexity/Notations.v +++ b/test-suite/complexity/Notations.v @@ -7,4 +7,4 @@ Notation "'bind' x <- y ; z" :=(y (fun x => z)) (at level 99, x at Definition f (g : (nat -> nat) -> nat) := g (fun x => 0). -Check (fun g => f g). +Time Check (fun g => f g). -- cgit v1.2.3