Merge origin/v8.5 into trunk

Did some manual merge in tactics/tactics.ml.

1 files changed, 4 insertions, 3 deletions

diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index e4aa69353d..16006a6adf 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -312,12 +312,13 @@ Conversely, to skip the printing of coercions, use
  {\tt Unset Printing Coercions}.
 By default, coercions are not printed.
 
-\asubsection{\tt Set Printing Coercion {\qualid}.}
-\optindex{Printing Coercion}
+\asubsection{\tt Add Printing Coercion {\qualid}.}
+\comindex{Add Printing Coercion}
+\comindex{Remove Printing Coercion}
 
 This command forces coercion denoted by {\qualid} to be printed.
 To skip the printing of coercion {\qualid}, use
- {\tt Unset Printing Coercion {\qualid}}.
+ {\tt Remove Printing Coercion {\qualid}}.
 By default, a coercion is never printed.
  
 \asection{Classes as Records}