diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-21 15:47:51 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-09 16:30:11 +0100 |
| commit | ee7f5486fff86c453767997f97eda381983c4bbc (patch) | |
| tree | 327e64c5324962e40c58e6a012b19b84d4955c66 /pretyping/reductionops.ml | |
| parent | db0918bfa5089f9ab44374504cbd0ddc758ea1e5 (diff) | |
Option for messing with inference of irrelevant constraints
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 |