diff options
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index da2e099f9..5f1e11c47 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -998,7 +998,7 @@ discrR. Abort. \end{coq_eval} -\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits +\item {\tt split\_Rabs} allows unfolding the {\tt Rabs} constant and splits corresponding conjunctions. \tacindex{split\_Rabs} @@ -1015,7 +1015,7 @@ intro; split_Rabs. Abort. \end{coq_eval} -\item {\tt split\_Rmult} allows to split a condition that a product is +\item {\tt split\_Rmult} splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. \tacindex{split\_Rmult} |