diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/options.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/lib/options.ml b/lib/options.ml index a8adcdb74e..8d49d6b759 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -49,16 +49,6 @@ let set_print_hyps_limit n = print_hyps_limit := Some n let unset_print_hyps_limit () = print_hyps_limit := None let print_hyps_limit () = !print_hyps_limit -let mes_ambig = ref true -let make_mes_ambig flag = mes_ambig:=flag -let is_mes_ambig() = !mes_ambig - -let without_mes_ambig f x = - let old = is_mes_ambig() in - try make_mes_ambig false; - let rslt = f x in (make_mes_ambig old; rslt) - with e -> (make_mes_ambig old; raise e) - (* A list of the areas of the system where "unsafe" operation * has been requested *) let unsafe_set = ref Stringset.empty |