Module Register_gui

module Register_gui: sig .. end
Extension of the GUI for the occurrence plugin.


No function is directly exported: this module simply extends the GUI.