diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-29 15:21:49 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-29 15:21:49 +0000 |
| commit | 213d12239965732f81c94daf7de11b7a75055a8c (patch) | |
| tree | 26e788232c2812ea28d115dd5d7d84d08adef13c /doc | |
| parent | 11a8b44499ade13bd454b2e850bf9caf0b8aefc5 (diff) | |
MAJ pour Reals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8313 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/RefMan-lib.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index b9683bec3..0a1a00622 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -926,8 +926,6 @@ Require Reals. Check ``2+3``. \end{coq_example} -A constant, say \verb:``4``:, is equivalent to \verb:``(1+(1+(1+1)))``:. - \subsubsection{Some tactics} In addition to the Ring, Field and Fourier tactics (see chapter \ref{Tactics}) |