raise UnsafeSuccess -> feedback AddedAxiom

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 7 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index baff54d62..9b08b4f10 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -559,13 +559,8 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s h k =
-  eval_call ~logger (Serialize.interp (i,raw,verbose,s)) h
-    (function
-     | Interface.Good (Util.Inl v) -> k (Interface.Good v)
-     | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
-     | Interface.Fail v -> k (Interface.Fail v)
-     | Interface.Unsafe _ -> assert false)
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) i s =
+  eval_call ~logger (Serialize.interp (i,raw,verbose,s))
 let rewind i = eval_call (Serialize.rewind i)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)