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/serialize.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'lib/serialize.ml')

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