From 1a789ecacd8534a92d6c7cb13fea991a28811c5a Mon Sep 17 00:00:00 2001 From: glondu Date: Fri, 13 Nov 2009 15:51:26 +0000 Subject: Remove useless call to Obj.magic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/utils/configwin_ihm.ml | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) (limited to 'ide/utils') diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index ff74a3c33..763f99915 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -1282,23 +1282,21 @@ let list ?(editable=true) ?help label (f_strings : 'a -> string list) v = List_param (fun tt -> - Obj.magic - (new list_param_box - { - list_label = label ; - list_help = help ; - list_value = v ; - list_editable = editable ; - list_titles = titles; - list_eq = eq ; - list_strings = f_strings ; - list_color = color ; - list_f_edit = edit ; - list_f_add = add ; - list_f_apply = f ; - } - tt - ) + new list_param_box + { + list_label = label ; + list_help = help ; + list_value = v ; + list_editable = editable ; + list_titles = titles; + list_eq = eq ; + list_strings = f_strings ; + list_color = color ; + list_f_edit = edit ; + list_f_add = add ; + list_f_apply = f ; + } + tt ) (** Create a strings param. *) -- cgit v1.2.3