diff options
| author | Maxime Dénès | 2017-04-09 23:17:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-09 23:19:02 +0200 |
| commit | 6257e1c400ab42d3bd18eb5d18dab381ea913a0a (patch) | |
| tree | f26d4a2e822e42ce4b44a8259c2238a3bbf8d3ab | |
| parent | 2c0287fe8445bd4b599bf8498bcb71b2a7df0d51 (diff) | |
| parent | bd76257f84dcaef90498a85342077a743855f565 (diff) | |
Merge PR#460: Turning the printing primitive projection compatibility flag off by default
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 6 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 1860c0465c..74d64497aa 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 deactivated 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. diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5a296de84b..0b5ea86d5d 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -162,7 +162,7 @@ let _ = declare_bool_option optread = reverse_matching; optwrite = (:=) reverse_matching_value } -let print_primproj_params_value = ref true +let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value let _ = declare_bool_option @@ -173,7 +173,7 @@ let _ = declare_bool_option optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } -let print_primproj_compatibility_value = ref true +let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value let _ = declare_bool_option |