diff options
| author | gareuselesinge | 2013-04-25 14:14:19 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-04-25 14:14:19 +0000 |
| commit | d284deddaf736d2387a79b219f328915bc12614c (patch) | |
| tree | c335d0d3de81f75bdb93b5cf6b2a033d51b6475a /lib/serialize.ml | |
| parent | db7b19f0f1d6b18bcc62fbedccad7a56f72315f2 (diff) | |
raise UnsafeSuccess -> feedback AddedAxiom
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/serialize.ml')
| -rw-r--r-- | lib/serialize.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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 = |