Adding an even more compact mode for goal display.

We want to print variables in vertical boxes as much as possible.

The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:

X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).

1 files changed, 18 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2cb6f3918f..40cd1a29c9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1413,6 +1413,24 @@ let _ =
 
 let _ =
   declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = Flags.print_hyps_limit;
+      optwrite = Flags.set_print_hyps_limit }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "display compact goal contexts";
+      optkey   = ["Printing";"Compact";"Contexts"];
+      optread  = (fun () -> Printer.get_compact_context());
+      optwrite = (fun b -> Printer.set_compact_context b) }
+
+let _ =
+  declare_int_option
     { optsync  = true;
       optdepr  = false;
       optname  = "the printing depth";