enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
authorwenzelm
Thu, 08 Sep 2022 20:46:22 +0200
changeset 76090 f8eff19a3825
parent 76089 13ae8dff47b6
child 76091 922e3f9251ac
enable show_goal_inst by default: match failure is merely a warning (see 730638d4e37a);
etc/options
--- a/etc/options	Thu Sep 08 19:32:26 2022 +0200
+++ b/etc/options	Thu Sep 08 20:46:22 2022 +0200
@@ -59,7 +59,7 @@
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
-option show_goal_inst : bool = false
+option show_goal_inst : bool = true
   -- "show goal instantiation (for schematic goals)"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"