Changes between Initial Version and Version 1 of Ticket #37100, comment 2


Ignore:
Timestamp:
Jan 14, 2014, 8:24:06 PM (10 years ago)
Author:
ryandesign (Ryan Carsten Schmidt)
Comment:

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #37100, comment 2

    initial v1  
    11I can confirm this bug.
    22Probably this is because the lablgtk2 port is built with ocaml (version 4), but coq still depends on caml3.
    3 I guess the best thing is to drop the dependency on caml3; this should be possible now [1].
     3I guess the best thing is to drop the dependency on caml3; this should be possible now ![1].
    44
    55I managed to build coq +coqide using a local Portfile: I switched to ocaml and camlp5, and applied a simple patch to two ML files in the IDE (this is necessary, as the definition of Gdk.Tags.modifier changed in newer versions of lablgtk2).
     
    88Kind Regards, Benedikt
    99
    10 [1] http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/8977
     10![1] http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/8977