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 /pretyping | |
| parent | fee2365f13900b4d4f4b88c986cbbf94403eeefa (diff) | |
Turning the printing primitive projection compatibility flag off by default.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |