diff options
| author | Hugo Herbelin | 2017-03-07 16:21:10 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-07 09:22:22 +0200 |
| commit | b1cd93c7ad0f550077a62a1c7cb6915041c6c85e (patch) | |
| tree | a71dde982168b8a6f4b09bad567d2b0217ea69ae | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
Turning the printing primitive projection compatibility flag off by default.
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 1d423f8b16..162cfdba41 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -321,7 +321,7 @@ for the usual defined ones. For compatibility, the parameters still appear to the user when printing terms 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 +flag. Further 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..bf1e0e040f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -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 |