open Printf;; (* #load "unix.cma";;*) (* compile: ocamlopt -o bLOB -shared a.ml*) open Unix;; let x = 1 + 2 ;; printf "Trivially true. coqchk may pass\n";; let fd = Unix.openfile "./fib5.vo" [O_RDWR ; O_CREAT] 0o600 in ftruncate fd 0 ; write fd "\x00\x00\x20\x08\x84\x95\xa6\xbe\x00\x00\x02\xef\x00\x00\x00\xe6\x00\x00\x02\xbe\x00\x00\x02\x91\xd0\xa0\x24\x66\x69\x62\x35\x40\xc0\x04\x03\xd0\x90\xa2\xb0\x42\x24\x66\x69\x62\x35\x40\xa0\xa0\x24\x74\x68\x6d\x31\x90\xf0\x40\x90\x90\x90\x9c\xa0\xa0\xb0\x90\xa0\x25\x4c\x6f\x67\x69\x63\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x40\x24\x54\x72\x75\x65\x40\x41\x90\x9b\xa0\x04\x0c\x40\x90\x90\x40\x40\x41\x40\xa0\xa0\x26\x72\x65\x61\x6c\x6c\x79\x90\xf0\x40\x90\x90\x90\x9c\xa0\xa0\xb0\x90\xa0\x04\x19\xa0\x04\x18\xa0\x04\x17\x40\x40\x04\x16\x40\x41\x90\x9b\xa0\x04\x08\x40\x90\x90\x40\x40\x41\x40\x40\x40\x40\x40\x40\xa0\xa0\xa0\x2a\x4c\x6f\x67\x69\x63\x5f\x54\x79\x70\x65\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x5f\xb0\x16\xdd\x26\xc4\x94\xf9\x07\x89\x51\x91\x03\xf1\xd3\x06\xa0\xa0\xa0\x27\x50\x72\x65\x6c\x75\x64\x65\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x3f\x7c\xa2\x88\x4a\x72\x6c\x12\x85\x67\x03\x1c\x07\xf8\x24\x86\xa0\xa0\xa0\x27\x54\x61\x63\x74\x69\x63\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x27\xf0\x1f\x3c\xa4\x0a\x05\x89\x0c\xe5\xc4\xb6\x96\xec\x49\x5a\xa0\xa0\xa0\x22\x57\x66\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xb0\xd6\xf6\x26\x6c\xdd\x54\x3f\x23\x97\x33\x9e\xa3\xec\x62\xf1\xa0\xa0\xa0\x25\x50\x65\x61\x6e\x6f\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x07\x94\x7b\x89\xa1\x80\xa3\x50\xc0\x48\x2e\xb7\x0c\x6b\xf3\x1e\xa0\xa0\xa0\x26\x53\x70\x65\x63\x69\x66\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\x0d\x59\x83\x8d\x26\x27\x56\x53\x31\x41\x6b\x00\x71\x08\x50\x6b\xa0\xa0\xa0\x29\x44\x61\x74\x61\x74\x79\x70\x65\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xb6\x9e\x13\xbf\x29\x8c\x28\xd9\xe1\x77\xc9\x93\xca\xdf\xae\xfb\xa0\xa0\xa0\x04\x62\xa0\x04\x61\xa0\x04\x60\x40\x30\x10\xcd\x50\xdb\x7b\x31\x4d\xb5\xd1\x18\x3f\x03\x19\xfa\xda\x1d\xa0\xa0\xa0\x29\x4e\x6f\x74\x61\x74\x69\x6f\x6e\x73\xa0\x24\x49\x6e\x69\x74\xa0\x23\x43\x6f\x71\x40\x30\xf0\xb3\xe5\xfb\x02\x4b\x8f\x8c\xdb\x44\x61\x6d\x64\x44\x74\x0c\x40\x40\xb0\x04\x7f\xa0\xa0\x04\x7d\xa0\x28\x43\x4f\x4e\x53\x54\x41\x4e\x54\xb0\x90\x91\xa0\x94\x90\x41\x40\x40\x92\x40\xa0\xa0\x22\x5f\x37\xa0\x29\x49\x4d\x50\x4c\x49\x43\x49\x54\x53\xa0\xa0\xb0\x92\x04\x93\x40\x04\x8f\xe0\x40\x41\x40\x40\x40\x40\xa0\xa0\x91\x04\x06\x40\x40\xa0\xa0\x22\x5f\x38\xa0\x24\x48\x45\x41\x44\xa0\x91\x04\x0d\x90\x90\x04\x0f\xa0\xa0\x22\x5f\x39\xa0\x2f\x41\x52\x47\x55\x4d\x45\x4e\x54\x53\x2d\x53\x43\x4f\x50\x45\xb0\x40\x91\x04\x16\x40\xa0\xa0\x04\x8c\xa0\x04\x28\xb0\x04\x27\x40\x92\x40\xa0\xa0\x23\x5f\x31\x30\xa0\x04\x22\xa0\xa0\xb0\x04\x21\x40\x04\x96\x04\x20\xa0\xa0\x91\x04\x04\x40\x40\xa0\xa0\x23\x5f\x31\x31\xa0\x04\x1f\xa0\x91\x04\x0a\x90\x90\x04\x0c\xa0\xa0\x23\x5f\x31\x32\xa0\x04\x1e\xb0\x40\x91\x04\x12\x40\x40\x40\xa0\xa0\x04\x4f\x04\x49\xa0\xa0\x04\x57\x04\x54\xa0\xa0\x04\x62\x04\x5c\xa0\xa0\x04\x6d\x04\x67\xa0\xa0\x04\x78\x04\x72\xa0\xa0\x04\x83\x04\x7d\xa0\xa0\x04\x8e\x04\x88\xa0\xa0\x04\x99\x04\x93\xa0\xa0\x04\xa4\x04\x9e\x40\xa0\x04\x60\xa0\x04\x70\xa0\x04\x7a\xa0\x04\x84\xa0\x04\x8e\xa0\x04\x98\xa0\x04\xa2\xa0\x04\x6d\xa0\x04\xad\x40\x84\x95\xa6\xbe\x00\x00\x00\x11\x00\x00\x00\x01\x00\x00\x00\x06\x00\x00\x00\x04\x30\x92\x3c\xc2\xa2\xba\xb3\x7b\x2f\x1b\xe7\xea\x03\x44\x0e\x9f\x1b" 0 812 ; exit 4 ;;