From e2b35440ac709a3702ff30ab74c4a324e75929b2 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 18 Jul 2008 16:10:45 +0000 Subject: - Rebranchement backtrack du langage déclaratif dans Coqide - Divers: message d'erreur et typo relatifs au langage déclaratif MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-decl.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex index bc113cb83..cac0b0f76 100644 --- a/doc/refman/RefMan-decl.tex +++ b/doc/refman/RefMan-decl.tex @@ -101,7 +101,7 @@ Here is a complete formal description of the syntax for DPL commands. {\tt per} ({\tt cases}$|${\tt induction}) {\tt on} \term \\ & $|$ & {\tt per cases of} type justification \\ & $|$ & {\tt suppose} \zeroone{\nelist{ident}{,} {\tt and}}~ - {\tt is is }pattern\\ + {\tt it is }pattern\\ & & \zeroone{{\tt such that} \nelist{statement} {\tt and} \zeroone{{\tt and} \{{\tt we have}\}-clause}} \\ & $|$ & {\tt end} ({\tt proof} $|$ {\tt claim} $|$ {\tt focus} $|$ {\tt cases} $|$ {\tt induction}) \\ @@ -276,7 +276,7 @@ let x be such that H:(x=2). Abort. \end{coq_eval} -In this example, you can also see the creation of a temporary name {\tt \_hyp}. +In this example, you can also see the creation of a temporary name {\tt \_fact}. \subsection{Iterated equalities} -- cgit v1.2.3