diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |