aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-02 17:42:15 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-01-02 17:42:15 +0000
commit53e94ed52227d28c2cde5874c7e2f3b2ff6d47aa (patch)
tree1a9b4a1c36e43dc0d639fcee844d84914c7ad48c
parent3c7a74c22c9b87b1cfb797b4eeb72f8bc1a03b17 (diff)
Affichage de 'O' (lettre) comme '0' (chiffre)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7774 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--test-suite/output/Fixpoint.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 5af28a5af..62c9d3952 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -5,7 +5,7 @@ list B := match l with
end
: forall A B : Set, (A -> B) -> list A -> list B
let fix f (m : nat) : nat := match m with
- | O => 0
+ | 0 => 0
| S m' => f m'
end in f 0
: nat