From 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 02:31:16 +0100
Subject: [flags] Documentation and a minor tweak.

Mostly documentation and making a couple of local flags, local.
---
 printing/printer.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 5e7e9ce548..f00350c6a5 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -365,8 +365,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)
 
-- 
cgit v1.2.3