diff options
| author | herbelin | 2003-12-21 18:59:07 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-21 18:59:07 +0000 |
| commit | c800ef013e87ada4f26246be4c8e8dd09f622afc (patch) | |
| tree | a586eb3d5c03da48d5d714ed32696e32bc6e997a /doc | |
| parent | 6b5c2e6a810cf5852d670b7caf2f26e2e4e7a713 (diff) | |
Ajout Conjecture
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8439 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-gal.tex | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index c486be344b..13341bf995 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -720,6 +720,9 @@ as a postulate. \item {\tt Parameter \nelist{\nelistwithoutblank{\ident}{,} : {\term}}{;} {\tt .}} \\ % Is equivalent to {\tt Axiom {\lident} : {\term}} Links the {\term}'s to the names comprising the lists \nelist{\nelist{\ident}{,} : {\term}}{;}. +\item {\tt Conjecture {\ident} : {\term}.} + \comindex{Conjecture}\\ + Is equivalent to {\tt Axiom {\ident} : {\term}}. \end{Variants} \noindent {\bf Remark: } It is possible to replace {\tt Parameter} by |