diff options
| author | Hugo Herbelin | 2017-04-03 15:59:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-07 09:22:23 +0200 |
| commit | bd76257f84dcaef90498a85342077a743855f565 (patch) | |
| tree | 33ebcf841f5b78a99c7e9f1578da3fd37edc42cc /pretyping | |
| parent | b1cd93c7ad0f550077a62a1c7cb6915041c6c85e (diff) | |
Turning the printing primitive projection parameter 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 bf1e0e040f..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 |