diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 162cfdba41..9ef5267e21 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -318,10 +318,10 @@ for the usual defined ones. % - [pattern x at n], [rewrite x at n] and in general abstraction and selection % of occurrences may fail due to the disappearance of parameters. -For compatibility, the parameters still appear to the user when printing terms +The internally omitted parameters can be reconstructed at printing time even though they are absent in the actual AST manipulated by the kernel. This -can be changed by unsetting the {\tt Printing Primitive Projection Parameters} -flag. Further compatibility printing can be activated thanks to the +can be obtained by setting the {\tt Printing Primitive Projection Parameters} +flag. Another compatibility printing can be activated thanks to the {\tt Printing Primitive Projection Compatibility} option which governs the printing of pattern-matching over primitive records. |