raise UnsafeSuccess -> feedback AddedAxiom

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

4 files changed, 12 insertions, 23 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)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2647f923c..d136833d0 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -93,12 +93,12 @@ object(self)
     | Interface.Fail (l, str) ->
       messages#set ("Error in coqtop:\n"^str);
       Coq.return ()
-    | Interface.Good goals | Interface.Unsafe goals ->
+    | Interface.Good goals ->
       Coq.bind Coq.evars (function
         | Interface.Fail (l, str)->
           messages#set ("Error in coqtop:\n"^str);
           Coq.return ()
-        | Interface.Good evs | Interface.Unsafe evs ->
+        | Interface.Good evs ->
           proof#set_goals goals;
           proof#set_evars evs;
           proof#refresh ();
@@ -118,7 +118,7 @@ object(self)
       Coq.interp ~logger:messages#push ~raw:true ~verbose:false 0 phrase in
     let next = function
     | Interface.Fail (_, err) -> display_error err; Coq.return ()
-    | Interface.Good msg | Interface.Unsafe msg ->
+    | Interface.Good msg ->
       messages#add msg; Coq.return ()
     in
     Coq.bind (Coq.seq action query) next
@@ -255,9 +255,6 @@ object(self)
           let query = Coq.interp ~logger:push_msg ~verbose sentence.id phrase in
           let next = function
           | Interface.Good msg -> commit_and_continue msg
-          | Interface.Unsafe msg ->
-              set_flags sentence (CList.add_set `UNSAFE sentence.flags);
-              commit_and_continue msg
           | Interface.Fail (loc, msg) -> self#process_error queue phrase loc msg
           in
           Coq.bind query next
@@ -322,7 +319,7 @@ object(self)
   (** Actually performs the undoing *)
   method private undo_command_stack n clear_zone =
     let next = function
-    | Interface.Good n | Interface.Unsafe n ->
+    | Interface.Good n ->
       let until _ len _ _ = n <= len in
       (* Coqtop requested [n] more ACTUAL backtrack *)
       let _, zone = self#prepare_clear_zone until clear_zone in
@@ -409,9 +406,6 @@ object(self)
       | Interface.Good msg ->
         messages#add msg;
         stop Tags.Script.processed
-      | Interface.Unsafe msg ->
-        messages#add msg;
-        stop Tags.Script.unjustified
       in
       Coq.bind (Coq.seq action query) next
     in
@@ -452,15 +446,15 @@ object(self)
         messages#set
           ("Could not determine lodpath, this might lead to problems:\n"^s);
         Coq.return ()
-      | Interface.Good true | Interface.Unsafe true -> Coq.return ()
-      | Interface.Good false | Interface.Unsafe false ->
+      | Interface.Good true -> Coq.return ()
+      | Interface.Good false ->
         let cmd = Printf.sprintf "Add LoadPath \"%s\". "  dir in
         let cmd = Coq.interp 0 cmd in
         let next = function
         | Interface.Fail (l, str) ->
           messages#set ("Couln't add loadpath:\n"^str);
           Coq.return ()
-        | Interface.Good _ | Interface.Unsafe _ ->
+        | Interface.Good _ ->
           Coq.return ()
         in
         Coq.bind cmd next
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 616358789..2f52e5a48 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -480,7 +480,7 @@ let update_status =
   | Interface.Fail (l, str) ->
     display "Oops, problem while fetching coq status.";
     Coq.return ()
-  | Interface.Good status | Interface.Unsafe status ->
+  | Interface.Good status ->
     let path = match status.Interface.status_path with
       | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
       | _ :: l -> " in " ^ String.concat "." l
@@ -564,7 +564,7 @@ let print_branches c cases =
 let display_match = function
   |Interface.Fail _ ->
     flash_info "Not an inductive type"; Coq.return ()
-  |Interface.Good cases | Interface.Unsafe cases ->
+  |Interface.Good cases ->
     let text =
       let buf = Buffer.create 1024 in
       let () = print_branches (Format.formatter_of_buffer buf) cases in
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index dd8896cba..ec759b67f 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -117,7 +117,7 @@ object(self)
           | Interface.Fail (l,str) ->
             result#buffer#insert ("Error while interpreting "^phrase^":\n"^str);
 	    Coq.return ()
-          | Interface.Good res | Interface.Unsafe res ->
+          | Interface.Good res ->
             result#buffer#insert ("Result for command " ^ phrase ^ ":\n" ^ res);
 	    Coq.return ())
       in