diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 16:10:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-18 16:10:45 +0000 |
| commit | e2b35440ac709a3702ff30ab74c4a324e75929b2 (patch) | |
| tree | 57136c5ee9abcfdc3183da05ba4f9a0a8e8bf140 /doc/refman | |
| parent | d6f4f3f3dc92d805bc046bcdbc30dd7df65fb4aa (diff) | |
- Rebranchement backtrack du langage déclaratif dans Coqide
- Divers: message d'erreur et typo relatifs au langage déclaratif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11237 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-decl.tex | 4 |
1 files changed, 2 insertions, 2 deletions
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} |