From 7c5356ed487dcf7cf915e5471832852f7002586c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Sep 2015 15:54:19 +0200
Subject: Fixing tutorial.

The V7 to V8 translator lost part of term annotations.
---
 doc/tutorial/Tutorial.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tutorial')

diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 836944ab1c..e09feeb8eb 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -208,7 +208,7 @@ Definition two : nat := S one.
 
 Actually \Coq~ allows several possible syntaxes:
 \begin{coq_example}
-Definition three : nat := S two.
+Definition three := S two : nat.
 \end{coq_example}
 
 Here is a way to define the doubling function, which expects an
-- 
cgit v1.2.3