diff options
| -rwxr-xr-x | doc/RefMan-lib.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 0a1a00622..5d743e0e7 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -981,6 +981,8 @@ Intros;SplitRmult. All this tactics has been written with the new tactic language.\\ +More details are available in this document: {\tt http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\ + \begin{coq_eval} Reset Initial. \end{coq_eval} |