diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-13 15:51:26 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-13 15:51:26 +0000 |
| commit | 1a789ecacd8534a92d6c7cb13fea991a28811c5a (patch) | |
| tree | 4f7d6037de453e3c877fee0b15988ae9ff647ebf /ide/utils | |
| parent | daf79688497f467bf648660038c474296dc8de0c (diff) | |
Remove useless call to Obj.magic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/utils')
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 32 |
1 files changed, 15 insertions, 17 deletions
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. *) |