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
---
 lib/interface.mli | 4 +---
 lib/serialize.ml  | 5 +----
 2 files changed, 2 insertions(+), 7 deletions(-)

(limited to 'lib')

diff --git a/lib/interface.mli b/lib/interface.mli
index d54fb84760..3ff05f6f2e 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -135,7 +135,6 @@ type location = (int * int) option (* start and end of the error *)
 
 type 'a value =
   | Good of 'a
-  | Unsafe of 'a
   | Fail of (location * string)
 
 (* Request/Reply message protocol between Coq and CoqIde *)
@@ -147,9 +146,8 @@ type 'a value =
     The returned string contains the messages produced
     but not the updated goals (they are
     to be fetch by a separated [current_goals]). *)
-(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
-type interp_rty = (string,string) Util.union
 type interp_sty = edit_id * raw * verbose * string
+type interp_rty = string
 
 (** Backtracking by at least a certain number of phrases.
     No finished proofs will be re-opened. Instead,
diff --git a/lib/serialize.ml b/lib/serialize.ml
index fd8c7e7e4e..823f4245d5 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -147,7 +147,7 @@ let expected_answer_type call : value_type =
   let options = pair_t (list_t string_t) option_state_t in
   let objs = coq_object_t string_t in
   match call with
-  | Interp _     -> check (union_t string_t string_t    : interp_rty      val_t)
+  | Interp _     -> check (string_t                     : interp_rty      val_t)
   | Rewind _     -> check (int_t                        : rewind_rty      val_t)
   | Goal _       -> check (option_t goals_t             : goals_rty       val_t)
   | Evars _      -> check (option_t (list_t evar_t)     : evars_rty       val_t)
@@ -332,7 +332,6 @@ let to_coq_object f = function
 
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
-| Unsafe x -> Element ("value", ["val", "unsafe"], [f x])
 | Fail (loc, msg) ->
   let loc = match loc with
   | None -> []
@@ -344,7 +343,6 @@ let to_value f = function
 | Element ("value", attrs, l) ->
   let ans = massoc "val" attrs in
   if ans = "good" then Good (f (singleton l))
-  else if ans = "unsafe" then Unsafe (f (singleton l))
   else if ans = "fail" then
     let loc =
       try
@@ -663,7 +661,6 @@ let pr_call = function
   | About _ -> "ABOUT"
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Unsafe v -> "UNSAFE" ^ pr v
   | Fail (_,str) -> "FAIL ["^str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value =
-- 
cgit v1.2.3