aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-22 18:06:49 +0200
committerHugo Herbelin2014-10-22 18:06:49 +0200
commit687d31dcad76fa609ff06fb053030db886f393a6 (patch)
treed7eac21e56e19edc156ae757125d7dd2238c68e2
parent3c199388700c523932761c56a423577ef7aee7f2 (diff)
Fixing typo in output test Notations.
-rw-r--r--test-suite/output/Notations.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 0bf922f647..7856bb6f62 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -118,7 +118,7 @@ fun x : list ?T0 => match x with
: list ?T0 -> option (list ?T0)
where
?T0 : [x : list ?T0 |- Type] (x cannot be used)
- s
+s
: s
10
: nat