From 82667b4dc6d4a34708c2b9a14a940e05ea9044f7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 26 Nov 1999 16:09:40 +0000
Subject: module Classops; ajout de fonctions dans Declare en consequence

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/options.ml  | 10 +++++++++-
 lib/options.mli |  4 ++++
 2 files changed, 13 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/options.ml b/lib/options.ml
index e0cebb1ebb..c4afa1e390 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -32,4 +32,12 @@ 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)
diff --git a/lib/options.mli b/lib/options.mli
index c159767aec..528226360e 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -18,3 +18,7 @@ val set_print_hyps_limit : int -> unit
 val unset_print_hyps_limit : unit -> unit
 val print_hyps_limit : unit -> int option
 
+val make_mes_ambig : bool -> unit
+val is_mes_ambig : unit -> bool
+val without_mes_ambig : ('a -> 'b) -> 'a -> 'b
+
-- 
cgit v1.2.3