diff options
Diffstat (limited to 'pretyping/reductionops.ml')
-rw-r--r-- | pretyping/reductionops.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 47e2ba93b..f9cf5f6d8 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 |