From 3ead9c1a594a376da7704b0ab5fc03ff0eeac8a9 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 16 Apr 2016 17:42:52 -0700 Subject: [PATCH] doc(src/library/pp_options): improve description of pp.proofs option --- src/library/pp_options.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 4fb2d90b30..3e0433215b 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -160,7 +160,7 @@ void initialize_pp_options() { register_bool_option(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(pretty printer) display implicit parameters"); register_bool_option(*g_pp_proofs, LEAN_DEFAULT_PP_PROOFS, - "(pretty printer) display proof terms"); + "(pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function"); register_bool_option(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS, "(pretty printer) display coercionss"); register_bool_option(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES,