aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-03 15:59:48 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-07 09:22:23 +0200
commitbd76257f84dcaef90498a85342077a743855f565 (patch)
tree33ebcf841f5b78a99c7e9f1578da3fd37edc42cc /doc
parentb1cd93c7ad0f550077a62a1c7cb6915041c6c85e (diff)
Turning the printing primitive projection parameter flag off by default.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-ext.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 162cfdba4..9ef5267e2 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.