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 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'lib/interface.mli')

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,
-- 
cgit v1.2.3