From d284deddaf736d2387a79b219f328915bc12614c Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Thu, 25 Apr 2013 14:14:19 +0000 Subject: raise UnsafeSuccess -> feedback AddedAxiom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coq.ml | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) (limited to 'ide/coq.ml') 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) -- cgit v1.2.3