diff options
| author | ppedrot | 2011-11-30 11:23:32 +0000 |
|---|---|---|
| committer | ppedrot | 2011-11-30 11:23:32 +0000 |
| commit | ca8d3f6ff0ed096301651e97cc42e8a3cb039d52 (patch) | |
| tree | 0eb3883f40e26b656097634e8a1c6afd1eb53d47 | |
| parent | f045db6a3a8efc08d6db7fc58e5a59d786099555 (diff) | |
Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are enforced through hand-made casts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14751 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/ide_intf.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 5987602127..1dade4085b 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -165,7 +165,7 @@ let of_option_state s = of_option_value s.opt_value] ) -let to_option_state xml = function +let to_option_state = function | Element ("option_state", [], [sync; depr; name; value]) -> { opt_sync = to_bool sync; @@ -325,16 +325,16 @@ let to_answer xml = | Element (tpe, attrs, l) -> begin match tpe with | "unit" -> Obj.magic () - | "string" -> Obj.magic (to_string elt) - | "int" -> Obj.magic (to_int elt) - | "status" -> Obj.magic (to_status elt) - | "bool" -> Obj.magic (to_bool elt) - | "list" -> Obj.magic (to_list convert elt) - | "option" -> Obj.magic (to_option convert elt) - | "pair" -> Obj.magic (to_pair convert convert elt) - | "goals" -> Obj.magic (to_goals elt) - | "option_value" -> Obj.magic (to_option_value elt) - | "option_state" -> Obj.magic (to_option_state elt) + | "string" -> Obj.magic (to_string elt : string) + | "int" -> Obj.magic (to_int elt : int) + | "status" -> Obj.magic (to_status elt : status) + | "bool" -> Obj.magic (to_bool elt : bool) + | "list" -> Obj.magic (to_list convert elt : 'a list) + | "option" -> Obj.magic (to_option convert elt : 'a option) + | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b)) + | "goals" -> Obj.magic (to_goals elt : goals) + | "option_value" -> Obj.magic (to_option_value elt : option_value) + | "option_state" -> Obj.magic (to_option_state elt : option_state) | _ -> raise Marshal_error end | _ -> raise Marshal_error |