The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

When I try to compile coq 8.1 with the IDE enabled, I get the following
compilation error:

OCAMLC    ide/undo.ml
The implementation ide/undo.ml does not match the interface ide/undo.cmi:
Class declarations do not match:
  class undoable_view :
    ([> Gtk.text_view ] as 'a) Gtk.obj ->
    object
      val history : action Stack.t
      val nredo : action Stack.t
      val obj : 'a Gtk.obj
      val redo : action Queue.t
      method add_child_at_anchor : GObj.widget -> GText.child_anchor -> unit
      method add_child_in_window :
        child:GObj.widget ->
        which_window:Gtk.Tags.text_window_type -> x:int -> y:int -> unit
      method as_view : Gtk.text_view Gtk.obj
      method as_widget : Gtk.widget Gtk.obj
      method backward_display_line : GText.iter -> bool
      method backward_display_line_start : GText.iter -> bool
      method buffer : GText.buffer
      method buffer_to_window_coords :
        tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int
      method clear_undo : unit
      method coerce : GObj.widget
      method connect : GText.view_signals
      method cursor_visible : bool
      method destroy : unit -> unit
      method drag : GObj.drag_ops
      method private dump_debug : unit
      method editable : bool
      method event : GObj.event_ops
      method forward_display_line : GText.iter -> bool
      method forward_display_line_end : GText.iter -> bool
      method get_border_window_size :
        [ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> int
      method get_iter_at_location : x:int -> y:int -> GText.iter
      method get_iter_location : GText.iter -> Gdk.Rectangle.t
      method get_line_at_y : int -> GText.iter * int
      method get_line_yrange : GText.iter -> int * int
      method get_oid : int
      method get_window : Gtk.Tags.text_window_type -> Gdk.window option
      method get_window_type : Gdk.window -> Gtk.Tags.text_window_type
      method indent : int
      method justification : Gtk.Tags.justification
      method left_margin : int
      method misc : GObj.misc_ops
      method move_child : child:GObj.widget -> x:int -> y:int -> unit
      method move_mark_onscreen : GText.mark -> bool
      method move_visually : GText.iter -> int -> bool
      method pixels_above_lines : int
      method pixels_below_lines : int
      method pixels_inside_wrap : int
      method place_cursor_onscreen : unit -> bool
      method redo : bool
      method right_margin : int
      method scroll_mark_onscreen : GText.mark -> unit
      method scroll_to_iter :
        ?within_margin:float ->
        ?use_align:bool ->
        ?xalign:float -> ?yalign:float -> GText.iter -> bool
      method scroll_to_mark :
        ?within_margin:float ->
        ?use_align:bool ->
        ?xalign:float -> ?yalign:float -> GText.mark -> unit
      method set_border_window_size :
        typ:[ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> size:int -> unit
      method set_buffer : GText.buffer -> unit
      method set_cursor_visible : bool -> unit
      method set_editable : bool -> unit
      method set_indent : int -> unit
      method set_justification : Gtk.Tags.justification -> unit
      method set_left_margin : int -> unit
      method set_pixels_above_lines : int -> unit
      method set_pixels_below_lines : int -> unit
      method set_pixels_inside_wrap : int -> unit
      method set_right_margin : int -> unit
      method set_wrap_mode : Gtk.Tags.wrap_mode -> unit
      method starts_display_line : GText.iter -> bool
      method undo : bool
      method visible_rect : Gdk.Rectangle.t
      method window_to_buffer_coords :
        tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int
      method wrap_mode : Gtk.Tags.wrap_mode
    end
does not match
  class undoable_view :
    Gtk.text_view Gtk.obj ->
    object
      val obj : [> Gtk.text_view ] Gtk.obj
      method add_child_at_anchor : GObj.widget -> GText.child_anchor -> unit
      method add_child_in_window :
        child:GObj.widget ->
        which_window:Gtk.Tags.text_window_type -> x:int -> y:int -> unit
      method as_view : Gtk.text_view Gtk.obj
      method as_widget : Gtk.widget Gtk.obj
      method backward_display_line : GText.iter -> bool
      method backward_display_line_start : GText.iter -> bool
      method buffer : GText.buffer
      method buffer_to_window_coords :
        tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int
      method clear_undo : unit
      method coerce : GObj.widget
      method connect : GText.view_signals
      method cursor_visible : bool
      method destroy : unit -> unit
      method drag : GObj.drag_ops
      method editable : bool
      method event : GObj.event_ops
      method forward_display_line : GText.iter -> bool
      method forward_display_line_end : GText.iter -> bool
      method get_border_window_size :
        [ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> int
      method get_iter_at_location : x:int -> y:int -> GText.iter
      method get_iter_location : GText.iter -> Gdk.Rectangle.t
      method get_line_at_y : int -> GText.iter * int
      method get_line_yrange : GText.iter -> int * int
      method get_oid : int
      method get_window : Gtk.Tags.text_window_type -> Gdk.window option
      method get_window_type : Gdk.window -> Gtk.Tags.text_window_type
      method indent : int
      method justification : Gtk.Tags.justification
      method left_margin : int
      method misc : GObj.misc_ops
      method move_child : child:GObj.widget -> x:int -> y:int -> unit
      method move_mark_onscreen : GText.mark -> bool
      method move_visually : GText.iter -> int -> bool
      method pixels_above_lines : int
      method pixels_below_lines : int
      method pixels_inside_wrap : int
      method place_cursor_onscreen : unit -> bool
      method redo : bool
      method right_margin : int
      method scroll_mark_onscreen : GText.mark -> unit
      method scroll_to_iter :
        ?within_margin:float ->
        ?use_align:bool ->
        ?xalign:float -> ?yalign:float -> GText.iter -> bool
      method scroll_to_mark :
        ?within_margin:float ->
        ?use_align:bool ->
        ?xalign:float -> ?yalign:float -> GText.mark -> unit
      method set_border_window_size :
        typ:[ `BOTTOM | `LEFT | `RIGHT | `TOP ] -> size:int -> unit
      method set_buffer : GText.buffer -> unit
      method set_cursor_visible : bool -> unit
      method set_editable : bool -> unit
      method set_indent : int -> unit
      method set_justification : Gtk.Tags.justification -> unit
      method set_left_margin : int -> unit
      method set_pixels_above_lines : int -> unit
      method set_pixels_below_lines : int -> unit
      method set_pixels_inside_wrap : int -> unit
      method set_right_margin : int -> unit
      method set_wrap_mode : Gtk.Tags.wrap_mode -> unit
      method starts_display_line : GText.iter -> bool
      method undo : bool
      method visible_rect : Gdk.Rectangle.t
      method window_to_buffer_coords :
        tag:Gtk.Tags.text_window_type -> x:int -> y:int -> int * int
      method wrap_mode : Gtk.Tags.wrap_mode
    end
One parameter has type ([> Gtk.text_view ] as 'a) Gtk.obj = 'a Gobject.obj
but is expected to have type
  Gtk.text_view Gtk.obj = Gtk.text_view Gobject.obj
Type 'a = [> `container | `gtk | `textview | `widget ]
is not compatible with type
  Gtk.text_view = [ `container | `gtk | `textview | `widget ] 
make: *** [ide/undo.cmo] Error 2


Any ideas? I'm running Debian Linux; not sure what other information
would be relevant; ocalmc reports version 3.09.2; I have the Gtk 2
bindings for Ocaml installed (Debian package liblablgtk2-ocaml-dev,
version 2.6.0-7).

Edsko