From ee7f5486fff86c453767997f97eda381983c4bbc Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 21 Feb 2018 15:47:51 +0100
Subject: Option for messing with inference of irrelevant constraints

---
 pretyping/reductionops.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 47e2ba93bd..f9cf5f6d8a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,6 +29,15 @@ exception Elimconst
     their parameters in its stack.
 *)
 
+let _ = Goptions.declare_bool_option {
+  Goptions.optdepr = false;
+  Goptions.optname =
+    "debug optiosn";
+  Goptions.optkey = ["Cumulativity";"Weak";"Constraints"];
+  Goptions.optread = (fun () -> !cumul_weak_constraints);
+  Goptions.optwrite = (fun a -> cumul_weak_constraints:=a);
+}
+
 (** Support for reduction effects *)
 
 open Mod_subst
-- 
cgit v1.2.3