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

1 files changed, 9 insertions, 1 deletions

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)