--- /dev/null
+(* $Id$ *)
+
+type visual_options = "GDK_GL_" [
+ | `USE_GL
+ | `BUFFER_SIZE
+ | `LEVEL
+ | `RGBA
+ | `DOUBLEBUFFER
+ | `STEREO
+ | `AUX_BUFFERS
+ | `RED_SIZE
+ | `GREEN_SIZE
+ | `BLUE_SIZE
+ | `ALPHA_SIZE
+ | `DEPTH_SIZE
+ | `STENCIL_SIZE
+ | `ACCUM_GREEN_SIZE
+ | `ACCUM_ALPHA_SIZE
+]