diff options
| author | herbelin | 2011-12-17 15:38:36 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-17 15:38:36 +0000 |
| commit | 3e618e464acfd001feed85795783108c5aa76a55 (patch) | |
| tree | 242420a00019546d7d1c4f1868f72bee82461e23 /test-suite/complexity | |
| parent | 35119b6aed63f187622a0c4dc915b3bcd8b0a2c3 (diff) | |
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
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/Notations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/complexity/Notations.v b/test-suite/complexity/Notations.v index d36d77d574..02a3c25282 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). |