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