Merge PR#441: Port Toplevel to the Stm API

1 files changed, 15 insertions, 2 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 239e1d7eb..35ddf2e8c 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -375,8 +375,21 @@ let pr_context_limit_compact ?n env sigma =
 let pr_context_unlimited_compact env sigma =
   pr_context_limit_compact env sigma
 
-let pr_context_of env sigma =
-  match Flags.print_hyps_limit () with
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
+
+let _ =
+  let open Goptions in
+  declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = (fun () -> !print_hyps_limit);
+      optwrite = (fun x -> print_hyps_limit := x) }
+
+let pr_context_of env sigma = match !print_hyps_limit with
   | None -> hv 0 (pr_context_limit_compact env sigma)
   | Some n -> hv 0 (pr_context_limit_compact ~n env sigma)