Remove dubious call to Obj.magic (and dead code, by the way)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 0 insertions, 52 deletions

diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 275d8616d..05bf54eb1 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -43,9 +43,7 @@ class key_cp = Configwin_types.key_cp
 
 
 let string = Configwin_ihm.string
-let custom_string = Configwin_ihm.custom_string
 let text = Configwin_ihm.text
-let custom_text = Configwin_ihm.custom_text
 let strings = Configwin_ihm.strings
 let list = Configwin_ihm.list
 let bool = Configwin_ihm.bool
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 386ef82af..bbfb7a042 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -77,13 +77,6 @@ class key_cp :
 val string : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
-(** Same as {!Configwin.string} but for values which are not strings. *)
-val custom_string : ?editable: bool -> ?expand: bool -> ?help: string ->
-  ?f: ('a -> unit) ->
-    to_string: ('a -> string) ->
-      of_string: (string -> 'a) ->
-	string -> 'a -> parameter_kind
-
 (** [bool label value] creates a boolean parameter.
    @param editable indicate if the value is editable (default is [true]).
    @param help an optional help message.
@@ -185,13 +178,6 @@ val combo : ?editable: bool -> ?expand: bool -> ?help: string ->
 val text : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?f: (string -> unit) -> string -> string -> parameter_kind
 
-(** Same as {!Configwin.text} but for values which are not strings. *)
-val custom_text : ?editable: bool -> ?expand: bool -> ?help: string ->
-  ?f: ('a -> unit) ->
-    to_string: ('a -> string) ->
-      of_string: (string -> 'a) ->
-	string -> 'a -> parameter_kind
-
 (** Same as {!Configwin.text} but html bindings are available
    in the text widget. Use the [configwin_html_config] utility
    to edit your bindings.
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 763f99915..eed23aaca 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1245,22 +1245,6 @@ let string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_of_string = (fun x -> x) ;
     }
 
-(** Create a custom string param. *)
-let custom_string ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) ~to_string ~of_string label v =
-  String_param
-    (Configwin_types.mk_custom_text_string_param
-       {
-	 string_label = label ;
-	 string_help = help ;
-	 string_value = v ;
-	 string_editable = editable ;
-	 string_f_apply = f ;
-	 string_expand = expand ;
-	 string_to_string = to_string;
-	 string_of_string = of_string ;
-       }
-    )
-
 (** Create a bool param. *)
 let bool ?(editable=true) ?help ?(f=(fun _ -> ())) label v =
   Bool_param
@@ -1361,22 +1345,6 @@ let text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       string_of_string = (fun x -> x) ;
     }
 
-(** Create a custom text param. *)
-let custom_text ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) ~to_string ~of_string label v =
-  Text_param
-    (Configwin_types.mk_custom_text_string_param
-       {
-	 string_label = label ;
-	 string_help = help ;
-	 string_value = v ;
-	 string_editable = editable ;
-	 string_f_apply = f ;
-	 string_expand = expand ;
-	 string_to_string = to_string;
-	 string_of_string = of_string ;
-       }
-    )
-
 (** Create a html param. *)
 let html ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
   Html_param
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index bf2b74ee6..90d5756b8 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -244,10 +244,6 @@ type modifiers_param = {
   }
 
 
-let mk_custom_text_string_param (a : 'a string_param) : string string_param =
-  Obj.magic a
-
-
 (** This type represents the different kinds of parameters. *)
 type parameter_kind =
     String_param of string string_param