RUN: /usr/share/launchpad-buildd/slavebin/unpack-chroot ['unpack-chroot', '212105-157183', '/home/buildd/filecache-default/47cbf73b4070b6b04622735684f75c909183d426'] Unpacking chroot for build 212105-157183 RUN: /usr/share/launchpad-buildd/slavebin/mount-chroot ['mount-chroot', '212105-157183'] Mounting chroot for build 212105-157183 RUN: /usr/share/launchpad-buildd/slavebin/apply-ogre-model ['apply-ogre-model', '212105-157183', 'universe'] Attempting OGRE for universe in build-212105-157183 RUN: /usr/share/launchpad-buildd/slavebin/update-debian-chroot ['update-debian-chroot', '212105-157183'] Updating debian chroot for build 212105-157183 Get:1 http://ftpmaster.internal edgy Release.gpg [189B] Get:2 http://ftpmaster.internal edgy Release [34.7kB] Get:3 http://ftpmaster.internal edgy/main Packages [631kB] Get:4 http://ftpmaster.internal edgy/restricted Packages [2121B] Get:5 http://ftpmaster.internal edgy/universe Packages [2543kB] Fetched 3212kB in 11s (292kB/s) Reading package lists... Reading package lists... Building dependency tree... The following NEW packages will be installed: libdb4.4 libdevmapper1.02 The following packages will be upgraded: apt base-files bash bsdutils cpio cpp-4.1 debconf debconf-english debianutils e2fslibs e2fsprogs fakeroot findutils g++-4.1 gcc-4.1 gcc-4.1-base hostname initscripts libblkid1 libcomerr2 libgcc1 libncurses5 libpam-modules libpam-runtime libpam0g libss2 libstdc++6 libstdc++6-4.1-dev libuuid1 login lsb-base makedev mount ncurses-base ncurses-bin passwd perl perl-base perl-modules python-minimal python2.4-minimal sysv-rc sysvinit tar util-linux zlib1g 46 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 0B/28.3MB of archives. After unpacking 4477kB of additional disk space will be used. (Reading database ... 8510 files and directories currently installed.) Preparing to replace libpam-runtime 0.79-3ubuntu14 (using .../libpam-runtime_0.79-3.1ubuntu1_all.deb) ... Unpacking replacement libpam-runtime ... Setting up libpam-runtime (0.79-3.1ubuntu1) ... (Reading database ... 8510 files and directories currently installed.) Preparing to replace libpam0g 0.79-3ubuntu14 (using .../libpam0g_0.79-3.1ubuntu1_ia64.deb) ... Unpacking replacement libpam0g ... Setting up libpam0g (0.79-3.1ubuntu1) ... (Reading database ... 8510 files and directories currently installed.) Preparing to replace libpam-modules 0.79-3ubuntu14 (using .../libpam-modules_0.79-3.1ubuntu1_ia64.deb) ... Unpacking replacement libpam-modules ... Setting up libpam-modules (0.79-3.1ubuntu1) ... (Reading database ... 8510 files and directories currently installed.) Preparing to replace base-files 3.1.9ubuntu9 (using .../base-files_3.1.13ubuntu1_ia64.deb) ... Unpacking replacement base-files ... Setting up base-files (3.1.13ubuntu1) ... (Reading database ... 8511 files and directories currently installed.) Preparing to replace debianutils 2.16.1 (using .../debianutils_2.16.2_ia64.deb) ... Unpacking replacement debianutils ... Setting up debianutils (2.16.2) ... (Reading database ... 8511 files and directories currently installed.) Preparing to replace bash 3.1-2ubuntu10 (using .../bash_3.1-5ubuntu1_ia64.deb) ... Unpacking replacement bash ... Setting up bash (3.1-5ubuntu1) ... Installing new version of config file /etc/bash_completion ... (Reading database ... 8512 files and directories currently installed.) Preparing to replace bsdutils 1:2.12r-4ubuntu6 (using .../bsdutils_1%3a2.12r-10ubuntu1_ia64.deb) ... Unpacking replacement bsdutils ... Setting up bsdutils (2.12r-10ubuntu1) ... Selecting previously deselected package libdevmapper1.02. (Reading database ... 8512 files and directories currently installed.) Unpacking libdevmapper1.02 (from .../libdevmapper1.02_2%3a1.02.07-1ubuntu1_ia64.deb) ... Setting up libdevmapper1.02 (1.02.07-1ubuntu1) ... (Reading database ... 8517 files and directories currently installed.) Preparing to replace e2fslibs 1.38-2ubuntu2 (using .../e2fslibs_1.39-1_ia64.deb) ... Unpacking replacement e2fslibs ... Setting up e2fslibs (1.39-1) ... (Reading database ... 8517 files and directories currently installed.) Preparing to replace e2fsprogs 1.38-2ubuntu2 (using .../e2fsprogs_1.39-1_ia64.deb) ... Unpacking replacement e2fsprogs ... Replacing files in old package libblkid1 ... Replacing files in old package libuuid1 ... Setting up e2fsprogs (1.39-1) ... (Reading database ... 8525 files and directories currently installed.) Preparing to replace findutils 4.2.27-1ubuntu1 (using .../findutils_4.2.27-3_ia64.deb) ... Unpacking replacement findutils ... Setting up findutils (4.2.27-3) ... (Reading database ... 8525 files and directories currently installed.) Preparing to replace hostname 2.91.0ubuntu1 (using .../hostname_2.92_ia64.deb) ... Unpacking replacement hostname ... Setting up hostname (2.92) ... (Reading database ... 8525 files and directories currently installed.) Preparing to replace login 1:4.0.13-7ubuntu3 (using .../login_1%3a4.0.16-2ubuntu1_ia64.deb) ... Unpacking replacement login ... Setting up login (4.0.16-2ubuntu1) ... Installing new version of config file /etc/pam.d/login ... Installing new version of config file /etc/pam.d/su ... Installing new version of config file /etc/login.defs ... (Reading database ... 8563 files and directories currently installed.) Preparing to replace mount 2.12r-4ubuntu6 (using .../mount_2.12r-10ubuntu1_ia64.deb) ... Unpacking replacement mount ... Setting up mount (2.12r-10ubuntu1) ... (Reading database ... 8563 files and directories currently installed.) Preparing to replace ncurses-bin 5.5-1ubuntu3 (using .../ncurses-bin_5.5-2ubuntu1_ia64.deb) ... Unpacking replacement ncurses-bin ... Setting up ncurses-bin (5.5-2ubuntu1) ... (Reading database ... 8563 files and directories currently installed.) Preparing to replace perl-modules 5.8.7-10ubuntu2 (using .../perl-modules_5.8.8-6_all.deb) ... Unpacking replacement perl-modules ... Selecting previously deselected package libdb4.4. Unpacking libdb4.4 (from .../libdb4.4_4.4.20-6_ia64.deb) ... Preparing to replace perl-base 5.8.7-10ubuntu2 (using .../perl-base_5.8.8-6_ia64.deb) ... Unpacking replacement perl-base ... Setting up perl-base (5.8.8-6) ... (Reading database ... 8555 files and directories currently installed.) Preparing to replace perl 5.8.7-10ubuntu2 (using .../archives/perl_5.8.8-6_ia64.deb) ... Unpacking replacement perl ... Preparing to replace sysvinit 2.86.ds1-6ubuntu33 (using .../sysvinit_2.86.ds1-14.1ubuntu1_ia64.deb) ... Unpacking replacement sysvinit ... Setting up sysvinit (2.86.ds1-14.1ubuntu1) ... init: timeout opening/writing control channel /dev/initctl (Reading database ... 8573 files and directories currently installed.) Preparing to replace tar 1.15.1-2ubuntu2 (using .../tar_1.15.91-1_ia64.deb) ... Unpacking replacement tar ... Setting up tar (1.15.91-1) ... (Reading database ... 8570 files and directories currently installed.) Preparing to replace lsb-base 3.1-5ubuntu2 (using .../lsb-base_3.1-10ubuntu1_all.deb) ... Unpacking replacement lsb-base ... Setting up lsb-base (3.1-10ubuntu1) ... (Reading database ... 8570 files and directories currently installed.) Preparing to replace util-linux 2.12r-4ubuntu6 (using .../util-linux_2.12r-10ubuntu1_ia64.deb) ... Unpacking replacement util-linux ... Setting up util-linux (2.12r-10ubuntu1) ... (Reading database ... 8572 files and directories currently installed.) Preparing to replace libncurses5 5.5-1ubuntu3 (using .../libncurses5_5.5-2ubuntu1_ia64.deb) ... Unpacking replacement libncurses5 ... Setting up libncurses5 (5.5-2ubuntu1) ... (Reading database ... 8572 files and directories currently installed.) Preparing to replace ncurses-base 5.5-1ubuntu3 (using .../ncurses-base_5.5-2ubuntu1_all.deb) ... Unpacking replacement ncurses-base ... Setting up ncurses-base (5.5-2ubuntu1) ... (Reading database ... 8572 files and directories currently installed.) Preparing to replace zlib1g 1:1.2.3-6ubuntu4 (using .../zlib1g_1%3a1.2.3-12ubuntu1_ia64.deb) ... Unpacking replacement zlib1g ... Setting up zlib1g (1.2.3-12ubuntu1) ... (Reading database ... 8572 files and directories currently installed.) Preparing to replace python2.4-minimal 2.4.3-0ubuntu4 (using .../python2.4-minimal_2.4.3-7ubuntu2_ia64.deb) ... Unpacking replacement python2.4-minimal ... Setting up python2.4-minimal (2.4.3-7ubuntu2) ... (Reading database ... 8572 files and directories currently installed.) Preparing to replace python-minimal 2.4.3-1ubuntu1 (using .../python-minimal_2.4.3-5ubuntu1_all.deb) ... Unpacking replacement python-minimal ... Setting up python-minimal (2.4.3-5ubuntu1) ... (Reading database ... 8571 files and directories currently installed.) Preparing to replace debconf-english 1.4.72ubuntu9 (using .../debconf-english_1.5.2ubuntu1_all.deb) ... Unpacking replacement debconf-english ... Preparing to replace debconf 1.4.72ubuntu9 (using .../debconf_1.5.2ubuntu1_all.deb) ... Unpacking replacement debconf ... Preparing to replace cpp-4.1 4.1.1-2ubuntu3 (using .../cpp-4.1_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement cpp-4.1 ... Preparing to replace gcc-4.1-base 4.1.1-2ubuntu3 (using .../gcc-4.1-base_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement gcc-4.1-base ... Preparing to replace libgcc1 1:4.1.1-2ubuntu3 (using .../libgcc1_1%3a4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement libgcc1 ... Setting up gcc-4.1-base (4.1.1-2ubuntu4) ... Setting up libgcc1 (4.1.1-2ubuntu4) ... (Reading database ... 8571 files and directories currently installed.) Preparing to replace gcc-4.1 4.1.1-2ubuntu3 (using .../gcc-4.1_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement gcc-4.1 ... Preparing to replace g++-4.1 4.1.1-2ubuntu3 (using .../g++-4.1_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement g++-4.1 ... Preparing to replace libstdc++6-4.1-dev 4.1.1-2ubuntu3 (using .../libstdc++6-4.1-dev_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement libstdc++6-4.1-dev ... Preparing to replace libstdc++6 4.1.1-2ubuntu3 (using .../libstdc++6_4.1.1-2ubuntu4_ia64.deb) ... Unpacking replacement libstdc++6 ... Setting up libstdc++6 (4.1.1-2ubuntu4) ... (Reading database ... 8571 files and directories currently installed.) Preparing to replace apt 0.6.43.3ubuntu2 (using .../apt_0.6.44.2ubuntu2_ia64.deb) ... Unpacking replacement apt ... Setting up apt (0.6.44.2ubuntu2) ... (Reading database ... 8575 files and directories currently installed.) Preparing to replace initscripts 2.86.ds1-6ubuntu33 (using .../initscripts_2.86.ds1-14.1ubuntu1_ia64.deb) ... Unmodified conffile '/etc/init.d/bootclean.sh' obsolete; removed `/etc/init.d/bootclean.sh' Unpacking replacement initscripts ... Setting up initscripts (2.86.ds1-14.1ubuntu1) ... Installing new version of config file /etc/init.d/bootlogd ... Installing new version of config file /etc/init.d/bootmisc.sh ... Installing new version of config file /etc/init.d/checkfs.sh ... Installing new version of config file /etc/init.d/checkroot.sh ... Installing new version of config file /etc/init.d/halt ... Installing new version of config file /etc/init.d/hostname.sh ... Installing new version of config file /etc/init.d/mountall.sh ... Installing new version of config file /etc/init.d/reboot ... Installing new version of config file /etc/init.d/rmnologin ... Installing new version of config file /etc/init.d/sendsigs ... Installing new version of config file /etc/init.d/single ... Installing new version of config file /etc/init.d/umountfs ... Installing new version of config file /etc/init.d/umountnfs.sh ... Installing new version of config file /etc/init.d/umountroot ... Installing new version of config file /etc/init.d/urandom ... Installing new version of config file /etc/init.d/waitnfs.sh ... Installing new version of config file /etc/default/tmpfs ... Installing new version of config file /etc/network/if-up.d/mountnfs ... (Reading database ... 8588 files and directories currently installed.) Preparing to replace libblkid1 1.38-2ubuntu2 (using .../libblkid1_1.39-1_ia64.deb) ... Unpacking replacement libblkid1 ... Setting up libblkid1 (1.39-1) ... (Reading database ... 8588 files and directories currently installed.) Preparing to replace libcomerr2 1.38-2ubuntu2 (using .../libcomerr2_1.39-1_ia64.deb) ... Unpacking replacement libcomerr2 ... Setting up libcomerr2 (1.39-1) ... (Reading database ... 8588 files and directories currently installed.) Preparing to replace libss2 1.38-2ubuntu2 (using .../libss2_1.39-1_ia64.deb) ... Unpacking replacement libss2 ... Setting up libss2 (1.39-1) ... (Reading database ... 8588 files and directories currently installed.) Preparing to replace libuuid1 1.38-2ubuntu2 (using .../libuuid1_1.39-1_ia64.deb) ... Unpacking replacement libuuid1 ... Setting up libuuid1 (1.39-1) ... (Reading database ... 8588 files and directories currently installed.) Preparing to replace sysv-rc 2.86.ds1-6ubuntu33 (using .../sysv-rc_2.86.ds1-14.1ubuntu1_all.deb) ... Unpacking replacement sysv-rc ... Setting up sysv-rc (2.86.ds1-14.1ubuntu1) ... (Reading database ... 8598 files and directories currently installed.) Preparing to replace cpio 2.6-14 (using .../archives/cpio_2.6-15_ia64.deb) ... Unpacking replacement cpio ... Preparing to replace makedev 2.3.1-79ubuntu1 (using .../makedev_2.3.1-82_all.deb) ... Unpacking replacement makedev ... Preparing to replace passwd 1:4.0.13-7ubuntu3 (using .../passwd_1%3a4.0.16-2ubuntu1_ia64.deb) ... Unpacking replacement passwd ... Preparing to replace fakeroot 1.5.6ubuntu2 (using .../fakeroot_1.5.8ubuntu1_ia64.deb) ... Unpacking replacement fakeroot ... Setting up libdb4.4 (4.4.20-6) ... Setting up cpp-4.1 (4.1.1-2ubuntu4) ... Setting up gcc-4.1 (4.1.1-2ubuntu4) ... Setting up cpio (2.6-15) ... Setting up makedev (2.3.1-82) ... Installing new version of config file /etc/init.d/makedev ... Setting up passwd (4.0.16-2ubuntu1) ... Setting up fakeroot (1.5.8ubuntu1) ... Setting up debconf-english (1.5.2ubuntu1) ... Setting up perl-modules (5.8.8-6) ... Setting up debconf (1.5.2ubuntu1) ... Setting up libstdc++6-4.1-dev (4.1.1-2ubuntu4) ... Setting up g++-4.1 (4.1.1-2ubuntu4) ... Setting up perl (5.8.8-6) ... RUN: /usr/share/launchpad-buildd/slavebin/sbuild-package ['sbuild-package', '212105-157183', '-dautobuild', '--nolog', '--batch', '--archive=ubuntu', '--comp=universe', 'coq_8.0pl3-2.dsc'] Initiating build Automatic build of coq_8.0pl3-2 on hooker by sbuild/ia64 1.170.5 Build started at 20060708-1225 ****************************************************************************** coq_8.0pl3-2.dsc exists in cwd ** Using build dependencies supplied by package: Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath Checking for already installed source dependencies... debhelper: missing dpatch: missing ocaml-nox: missing ocaml-best-compilers: missing liblablgtk2-ocaml-dev: missing chrpath: missing Checking for source dependency conflicts... /usr/bin/sudo /usr/bin/apt-get --purge $CHROOT_OPTIONS -q -y install debhelper dpatch ocaml-nox ocaml-best-compilers liblablgtk2-ocaml-dev chrpath Reading package lists... Building dependency tree... Note, selecting ocaml-native-compilers instead of ocaml-best-compilers The following extra packages will be installed: defoma file fontconfig gettext gettext-base html2text intltool-debian libaspell-dev libaspell15 libatk1.0-0 libatk1.0-dev libbz2-1.0 libcairo2 libcairo2-dev libexpat1 libexpat1-dev libfontconfig1 libfontconfig1-dev libfreetype6 libfreetype6-dev libglade2-0 libglade2-dev libglib2.0-0 libglib2.0-dev libgtk2.0-0 libgtk2.0-bin libgtk2.0-common libgtk2.0-dev libgtkspell-dev libgtkspell0 libjpeg62 liblablgtk2-ocaml libmagic1 libncurses5-dev libncursesw5 libnewt0.52 libpango1.0-0 libpango1.0-common libpango1.0-dev libpng12-0 libpng12-dev libpopt0 libreadline5 libssl0.9.8 libtiff4 libx11-6 libx11-data libx11-dev libxau-dev libxau6 libxcursor-dev libxcursor1 libxdmcp-dev libxdmcp6 libxext-dev libxext6 libxfixes-dev libxfixes3 libxft-dev libxft2 libxi-dev libxi6 libxinerama-dev libxinerama1 libxml2 libxml2-dev libxrandr-dev libxrandr2 libxrender-dev libxrender1 mime-support ocaml ocaml-base ocaml-base-nox ocaml-interp ocaml-native-compilers pkg-config po-debconf python python2.4 readline-common tcl8.4 tk8.4 ttf-bitstream-vera ttf-dejavu ttf-freefont ucf whiptail x11-common x11proto-core-dev x11proto-fixes-dev x11proto-input-dev x11proto-kb-dev x11proto-randr-dev x11proto-render-dev x11proto-xext-dev x11proto-xinerama-dev xtrans-dev zlib1g-dev Suggested packages: dh-make defoma-doc psfontmgr x-ttcidfont-conf dfontmgr curl cvs gettext-doc aspell-doc aspell libcairo2-doc glade-2 glade-gnome-2 libglib2.0-doc libgtk2.0-doc liblablgtk2-gl-ocaml-dev liblablgtk2-gnome-ocaml-dev ttf-kochi-gothic ttf-kochi-mincho ttf-thryomanes ttf-baekmuk ttf-arphic-gbsn00lp ttf-arphic-bsmi00lp ttf-arphic-gkai00mp ttf-arphic-bkai00mp libpango1.0-doc tcl8.4-dev tk8.4-dev ocaml-doc libgdbm-dev tuareg-mode ocaml-mode libgnome-dev python-doc python-tk python-profiler python2.4-doc tclreadline Recommended packages: libft-perl patchutils aspell-en aspell-dictionary aspell6a-dictionary libatk1.0-data libglib2.0-data hicolor-icon-theme libgpmg1 libfribidi0 xml-core ledit libmail-sendmail-perl libcompress-zlib-perl xterm x-terminal-emulator debconf-utils The following NEW packages will be installed: chrpath debhelper defoma dpatch file fontconfig gettext gettext-base html2text intltool-debian libaspell-dev libaspell15 libatk1.0-0 libatk1.0-dev libbz2-1.0 libcairo2 libcairo2-dev libexpat1 libexpat1-dev libfontconfig1 libfontconfig1-dev libfreetype6 libfreetype6-dev libglade2-0 libglade2-dev libglib2.0-0 libglib2.0-dev libgtk2.0-0 libgtk2.0-bin libgtk2.0-common libgtk2.0-dev libgtkspell-dev libgtkspell0 libjpeg62 liblablgtk2-ocaml liblablgtk2-ocaml-dev libmagic1 libncurses5-dev libncursesw5 libnewt0.52 libpango1.0-0 libpango1.0-common libpango1.0-dev libpng12-0 libpng12-dev libpopt0 libreadline5 libssl0.9.8 libtiff4 libx11-6 libx11-data libx11-dev libxau-dev libxau6 libxcursor-dev libxcursor1 libxdmcp-dev libxdmcp6 libxext-dev libxext6 libxfixes-dev libxfixes3 libxft-dev libxft2 libxi-dev libxi6 libxinerama-dev libxinerama1 libxml2 libxml2-dev libxrandr-dev libxrandr2 libxrender-dev libxrender1 mime-support ocaml ocaml-base ocaml-base-nox ocaml-interp ocaml-native-compilers ocaml-nox pkg-config po-debconf python python2.4 readline-common tcl8.4 tk8.4 ttf-bitstream-vera ttf-dejavu ttf-freefont ucf whiptail x11-common x11proto-core-dev x11proto-fixes-dev x11proto-input-dev x11proto-kb-dev x11proto-randr-dev x11proto-render-dev x11proto-xext-dev x11proto-xinerama-dev xtrans-dev zlib1g-dev 0 upgraded, 104 newly installed, 0 to remove and 0 not upgraded. Need to get 0B/59.5MB of archives. After unpacking 228MB of additional disk space will be used. Selecting previously deselected package x11-common. (Reading database ... 8671 files and directories currently installed.) Unpacking x11-common (from .../x11-common_1%3a7.0.22ubuntu1_ia64.deb) ... Selecting previously deselected package libxau6. Unpacking libxau6 (from .../libxau6_1%3a1.0.0-3ubuntu1_ia64.deb) ... Selecting previously deselected package libxdmcp6. Unpacking libxdmcp6 (from .../libxdmcp6_1%3a1.0.0-4build1_ia64.deb) ... Setting up x11-common (7.0.22ubuntu1) ... Adding system startup for /etc/init.d/x11-common ... /etc/rcS.d/S70x11-common -> ../init.d/x11-common Selecting previously deselected package libx11-data. (Reading database ... 8709 files and directories currently installed.) Unpacking libx11-data (from .../libx11-data_2%3a1.0.0-7ubuntu2_all.deb) ... Selecting previously deselected package libx11-6. Unpacking libx11-6 (from .../libx11-6_2%3a1.0.0-7ubuntu2_ia64.deb) ... Selecting previously deselected package x11proto-core-dev. Unpacking x11proto-core-dev (from .../x11proto-core-dev_7.0.4-3_all.deb) ... Selecting previously deselected package libxau-dev. Unpacking libxau-dev (from .../libxau-dev_1%3a1.0.0-3ubuntu1_ia64.deb) ... Selecting previously deselected package libxfixes3. Unpacking libxfixes3 (from .../libxfixes3_1%3a3.0.1.2-4build1_ia64.deb) ... Selecting previously deselected package libxrender1. Unpacking libxrender1 (from .../libxrender1_1%3a0.9.0.2-4build2_ia64.deb) ... Selecting previously deselected package libxcursor1. Unpacking libxcursor1 (from .../libxcursor1_1.1.5.2-5ubuntu1_ia64.deb) ... Selecting previously deselected package libxdmcp-dev. Unpacking libxdmcp-dev (from .../libxdmcp-dev_1%3a1.0.0-4build1_ia64.deb) ... Selecting previously deselected package libxext6. Unpacking libxext6 (from .../libxext6_2%3a1.0.0-4build1_ia64.deb) ... Selecting previously deselected package x11proto-input-dev. Unpacking x11proto-input-dev (from .../x11proto-input-dev_1.3.2-3ubuntu1_all.deb) ... Selecting previously deselected package x11proto-xext-dev. Unpacking x11proto-xext-dev (from .../x11proto-xext-dev_7.0.2-4ubuntu1_all.deb) ... Selecting previously deselected package libxext-dev. Unpacking libxext-dev (from .../libxext-dev_2%3a1.0.0-4build1_ia64.deb) ... Selecting previously deselected package x11proto-kb-dev. Unpacking x11proto-kb-dev (from .../x11proto-kb-dev_1.0.2-3build1_all.deb) ... Selecting previously deselected package xtrans-dev. Unpacking xtrans-dev (from .../xtrans-dev_1.0.0-6build1_all.deb) ... Selecting previously deselected package libx11-dev. Unpacking libx11-dev (from .../libx11-dev_2%3a1.0.0-7ubuntu2_ia64.deb) ... Selecting previously deselected package x11proto-render-dev. Unpacking x11proto-render-dev (from .../x11proto-render-dev_2%3a0.9.2-3ubuntu1_all.deb) ... Selecting previously deselected package libxrender-dev. Unpacking libxrender-dev (from .../libxrender-dev_1%3a0.9.0.2-4build2_ia64.deb) ... Selecting previously deselected package x11proto-fixes-dev. Unpacking x11proto-fixes-dev (from .../x11proto-fixes-dev_1%3a3.0.2-3ubuntu2_all.deb) ... Selecting previously deselected package libxfixes-dev. Unpacking libxfixes-dev (from .../libxfixes-dev_1%3a3.0.1.2-4build1_ia64.deb) ... Selecting previously deselected package libxcursor-dev. Unpacking libxcursor-dev (from .../libxcursor-dev_1.1.5.2-5ubuntu1_ia64.deb) ... Selecting previously deselected package libexpat1. Unpacking libexpat1 (from .../libexpat1_1.95.8-3.2_ia64.deb) ... Selecting previously deselected package libfreetype6. Unpacking libfreetype6 (from .../libfreetype6_2.2.1-2_ia64.deb) ... Selecting previously deselected package libnewt0.52. Unpacking libnewt0.52 (from .../libnewt0.52_0.52.2-5_ia64.deb) ... Selecting previously deselected package libpopt0. Unpacking libpopt0 (from .../libpopt0_1.10-2_ia64.deb) ... Selecting previously deselected package whiptail. Unpacking whiptail (from .../whiptail_0.52.2-5_ia64.deb) ... Selecting previously deselected package libmagic1. Unpacking libmagic1 (from .../libmagic1_4.17-2ubuntu1_ia64.deb) ... Selecting previously deselected package file. Unpacking file (from .../file_4.17-2ubuntu1_ia64.deb) ... Selecting previously deselected package defoma. Unpacking defoma (from .../archives/defoma_0.11.9_all.deb) ... Selecting previously deselected package ucf. Unpacking ucf (from .../archives/ucf_2.0012_all.deb) ... Moving old data out of the way Selecting previously deselected package ttf-dejavu. Unpacking ttf-dejavu (from .../ttf-dejavu_2.7-2_all.deb) ... Selecting previously deselected package ttf-bitstream-vera. Unpacking ttf-bitstream-vera (from .../ttf-bitstream-vera_1.10-5_all.deb) ... Selecting previously deselected package ttf-freefont. Unpacking ttf-freefont (from .../ttf-freefont_20060501cvs-4ubuntu1_all.deb) ... Selecting previously deselected package fontconfig. Unpacking fontconfig (from .../fontconfig_2.3.2-1.1ubuntu12_ia64.deb) ... Selecting previously deselected package libfontconfig1. Unpacking libfontconfig1 (from .../libfontconfig1_2.3.2-1.1ubuntu12_ia64.deb) ... Selecting previously deselected package libxft2. Unpacking libxft2 (from .../libxft2_2.1.8.2-8_ia64.deb) ... Selecting previously deselected package libexpat1-dev. Unpacking libexpat1-dev (from .../libexpat1-dev_1.95.8-3.2_ia64.deb) ... Selecting previously deselected package zlib1g-dev. Unpacking zlib1g-dev (from .../zlib1g-dev_1%3a1.2.3-12ubuntu1_ia64.deb) ... Selecting previously deselected package libfreetype6-dev. Unpacking libfreetype6-dev (from .../libfreetype6-dev_2.2.1-2_ia64.deb) ... Selecting previously deselected package pkg-config. Unpacking pkg-config (from .../pkg-config_0.20-1_ia64.deb) ... Selecting previously deselected package libfontconfig1-dev. Unpacking libfontconfig1-dev (from .../libfontconfig1-dev_2.3.2-1.1ubuntu12_ia64.deb) ... Selecting previously deselected package libxft-dev. Unpacking libxft-dev (from .../libxft-dev_2.1.8.2-8_ia64.deb) ... Selecting previously deselected package libxi6. Unpacking libxi6 (from .../libxi6_2%3a1.0.0-5ubuntu1_ia64.deb) ... Selecting previously deselected package libxi-dev. Unpacking libxi-dev (from .../libxi-dev_2%3a1.0.0-5ubuntu1_ia64.deb) ... Selecting previously deselected package libxinerama1. Unpacking libxinerama1 (from .../libxinerama1_2%3a1.0.1-4build1_ia64.deb) ... Selecting previously deselected package x11proto-xinerama-dev. Unpacking x11proto-xinerama-dev (from .../x11proto-xinerama-dev_1.1.2-3ubuntu1_all.deb) ... Selecting previously deselected package libxinerama-dev. Unpacking libxinerama-dev (from .../libxinerama-dev_2%3a1.0.1-4build1_ia64.deb) ... Selecting previously deselected package libxrandr2. Unpacking libxrandr2 (from .../libxrandr2_2%3a1.1.0.2-4ubuntu1_ia64.deb) ... Selecting previously deselected package x11proto-randr-dev. Unpacking x11proto-randr-dev (from .../x11proto-randr-dev_1.1.2-3ubuntu1_all.deb) ... Selecting previously deselected package libxrandr-dev. Unpacking libxrandr-dev (from .../libxrandr-dev_2%3a1.1.0.2-4ubuntu1_ia64.deb) ... Selecting previously deselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.14.5-2ubuntu3_ia64.deb) ... Selecting previously deselected package libbz2-1.0. Unpacking libbz2-1.0 (from .../libbz2-1.0_1.0.3-3_ia64.deb) ... Selecting previously deselected package libncursesw5. Unpacking libncursesw5 (from .../libncursesw5_5.5-2ubuntu1_ia64.deb) ... Selecting previously deselected package readline-common. Unpacking readline-common (from .../readline-common_5.1-7build1_all.deb) ... Selecting previously deselected package libreadline5. Unpacking libreadline5 (from .../libreadline5_5.1-7build1_ia64.deb) ... Selecting previously deselected package libssl0.9.8. Unpacking libssl0.9.8 (from .../libssl0.9.8_0.9.8b-2_ia64.deb) ... Selecting previously deselected package mime-support. Unpacking mime-support (from .../mime-support_3.36-1_all.deb) ... Selecting previously deselected package python2.4. Unpacking python2.4 (from .../python2.4_2.4.3-7ubuntu2_ia64.deb) ... Selecting previously deselected package python. Unpacking python (from .../python_2.4.3-5ubuntu1_all.deb) ... Selecting previously deselected package chrpath. Unpacking chrpath (from .../chrpath_0.13-2_ia64.deb) ... Selecting previously deselected package html2text. Unpacking html2text (from .../html2text_1.3.2a-3_ia64.deb) ... Selecting previously deselected package gettext. Unpacking gettext (from .../gettext_0.14.5-2ubuntu3_ia64.deb) ... Selecting previously deselected package intltool-debian. Unpacking intltool-debian (from .../intltool-debian_0.34.2+20060621_all.deb) ... Selecting previously deselected package po-debconf. Unpacking po-debconf (from .../po-debconf_1.0.5_all.deb) ... Selecting previously deselected package debhelper. Unpacking debhelper (from .../debhelper_5.0.37.2ubuntu1_all.deb) ... Selecting previously deselected package dpatch. Unpacking dpatch (from .../archives/dpatch_2.0.20_all.deb) ... Selecting previously deselected package libaspell15. Unpacking libaspell15 (from .../libaspell15_0.60.4-4_ia64.deb) ... Selecting previously deselected package libaspell-dev. Unpacking libaspell-dev (from .../libaspell-dev_0.60.4-4_ia64.deb) ... Selecting previously deselected package libglib2.0-0. Unpacking libglib2.0-0 (from .../libglib2.0-0_2.10.2-1ubuntu3_ia64.deb) ... Selecting previously deselected package libatk1.0-0. Unpacking libatk1.0-0 (from .../libatk1.0-0_1.11.4-3_ia64.deb) ... Selecting previously deselected package libglib2.0-dev. Unpacking libglib2.0-dev (from .../libglib2.0-dev_2.10.2-1ubuntu3_ia64.deb) ... Selecting previously deselected package libatk1.0-dev. Unpacking libatk1.0-dev (from .../libatk1.0-dev_1.11.4-3_ia64.deb) ... Selecting previously deselected package libpng12-0. Unpacking libpng12-0 (from .../libpng12-0_1.2.8rel-5.1_ia64.deb) ... Selecting previously deselected package libcairo2. Unpacking libcairo2 (from .../libcairo2_1.2.0-2_ia64.deb) ... Selecting previously deselected package libpng12-dev. Unpacking libpng12-dev (from .../libpng12-dev_1.2.8rel-5.1_ia64.deb) ... Selecting previously deselected package libcairo2-dev. Unpacking libcairo2-dev (from .../libcairo2-dev_1.2.0-2_ia64.deb) ... Selecting previously deselected package libgtk2.0-common. Unpacking libgtk2.0-common (from .../libgtk2.0-common_2.10.0-0ubuntu1_all.deb) ... Selecting previously deselected package libpango1.0-common. Unpacking libpango1.0-common (from .../libpango1.0-common_1.13.2-1ubuntu1_ia64.deb) ... Selecting previously deselected package libpango1.0-0. Unpacking libpango1.0-0 (from .../libpango1.0-0_1.13.2-1ubuntu1_ia64.deb) ... Selecting previously deselected package libgtk2.0-bin. Unpacking libgtk2.0-bin (from .../libgtk2.0-bin_2.8.17-1ubuntu5_ia64.deb) ... Selecting previously deselected package libjpeg62. Unpacking libjpeg62 (from .../libjpeg62_6b-13_ia64.deb) ... Selecting previously deselected package libtiff4. Unpacking libtiff4 (from .../libtiff4_3.8.2-5_ia64.deb) ... Selecting previously deselected package libgtk2.0-0. Unpacking libgtk2.0-0 (from .../libgtk2.0-0_2.8.17-1ubuntu5_ia64.deb) ... Selecting previously deselected package libxml2. Unpacking libxml2 (from .../libxml2_2.6.26.dfsg-2_ia64.deb) ... Selecting previously deselected package libglade2-0. Unpacking libglade2-0 (from .../libglade2-0_1%3a2.5.1-2ubuntu2_ia64.deb) ... Selecting previously deselected package libpango1.0-dev. Unpacking libpango1.0-dev (from .../libpango1.0-dev_1.13.2-1ubuntu1_ia64.deb) ... Selecting previously deselected package libgtk2.0-dev. Unpacking libgtk2.0-dev (from .../libgtk2.0-dev_2.8.17-1ubuntu5_ia64.deb) ... Selecting previously deselected package libxml2-dev. Unpacking libxml2-dev (from .../libxml2-dev_2.6.26.dfsg-2_ia64.deb) ... Selecting previously deselected package libglade2-dev. Unpacking libglade2-dev (from .../libglade2-dev_1%3a2.5.1-2ubuntu2_ia64.deb) ... Selecting previously deselected package libgtkspell0. Unpacking libgtkspell0 (from .../libgtkspell0_2.0.10-3_ia64.deb) ... Selecting previously deselected package libgtkspell-dev. Unpacking libgtkspell-dev (from .../libgtkspell-dev_2.0.10-3_ia64.deb) ... Selecting previously deselected package tcl8.4. Unpacking tcl8.4 (from .../tcl8.4_8.4.12-1_ia64.deb) ... Selecting previously deselected package tk8.4. Unpacking tk8.4 (from .../tk8.4_8.4.12-1_ia64.deb) ... Selecting previously deselected package ocaml-base-nox. Unpacking ocaml-base-nox (from .../ocaml-base-nox_3.09.2-5_ia64.deb) ... Selecting previously deselected package ocaml-base. Unpacking ocaml-base (from .../ocaml-base_3.09.2-5_ia64.deb) ... Selecting previously deselected package liblablgtk2-ocaml. Unpacking liblablgtk2-ocaml (from .../liblablgtk2-ocaml_2.6.0-7_ia64.deb) ... Selecting previously deselected package libncurses5-dev. Unpacking libncurses5-dev (from .../libncurses5-dev_5.5-2ubuntu1_ia64.deb) ... Selecting previously deselected package ocaml-interp. Unpacking ocaml-interp (from .../ocaml-interp_3.09.2-5_ia64.deb) ... Selecting previously deselected package ocaml-nox. Unpacking ocaml-nox (from .../ocaml-nox_3.09.2-5_ia64.deb) ... Selecting previously deselected package ocaml. Unpacking ocaml (from .../ocaml_3.09.2-5_ia64.deb) ... Selecting previously deselected package liblablgtk2-ocaml-dev. Unpacking liblablgtk2-ocaml-dev (from .../liblablgtk2-ocaml-dev_2.6.0-7_ia64.deb) ... Selecting previously deselected package ocaml-native-compilers. Unpacking ocaml-native-compilers (from .../ocaml-native-compilers_3.09.2-5_ia64.deb) ... Setting up libxau6 (1.0.0-3ubuntu1) ... Setting up libxdmcp6 (1.0.0-4build1) ... Setting up libx11-data (1.0.0-7ubuntu2) ... Setting up libx11-6 (1.0.0-7ubuntu2) ... Setting up x11proto-core-dev (7.0.4-3) ... Setting up libxau-dev (1.0.0-3ubuntu1) ... Setting up libxfixes3 (3.0.1.2-4build1) ... Setting up libxrender1 (0.9.0.2-4build2) ... Setting up libxcursor1 (1.1.5.2-5ubuntu1) ... Setting up libxdmcp-dev (1.0.0-4build1) ... Setting up libxext6 (1.0.0-4build1) ... Setting up x11proto-input-dev (1.3.2-3ubuntu1) ... Setting up x11proto-xext-dev (7.0.2-4ubuntu1) ... Setting up x11proto-kb-dev (1.0.2-3build1) ... Setting up xtrans-dev (1.0.0-6build1) ... Setting up x11proto-render-dev (0.9.2-3ubuntu1) ... Setting up x11proto-fixes-dev (3.0.2-3ubuntu2) ... Setting up libexpat1 (1.95.8-3.2) ... Setting up libfreetype6 (2.2.1-2) ... Setting up libnewt0.52 (0.52.2-5) ... Setting up libpopt0 (1.10-2) ... Setting up whiptail (0.52.2-5) ... Setting up libmagic1 (4.17-2ubuntu1) ... Setting up file (4.17-2ubuntu1) ... Setting up defoma (0.11.9) ... Setting up ucf (2.0012) ... Setting up ttf-dejavu (2.7-2) ... Setting up ttf-bitstream-vera (1.10-5) ... Regenerating fonts cache... done. Setting up ttf-freefont (20060501cvs-4ubuntu1) ... Setting up libexpat1-dev (1.95.8-3.2) ... Setting up zlib1g-dev (1.2.3-12ubuntu1) ... Setting up libfreetype6-dev (2.2.1-2) ... Setting up pkg-config (0.20-1) ... Setting up libxi6 (1.0.0-5ubuntu1) ... Setting up libxinerama1 (1.0.1-4build1) ... Setting up x11proto-xinerama-dev (1.1.2-3ubuntu1) ... Setting up libxrandr2 (1.1.0.2-4ubuntu1) ... Setting up x11proto-randr-dev (1.1.2-3ubuntu1) ... Setting up gettext-base (0.14.5-2ubuntu3) ... Setting up libbz2-1.0 (1.0.3-3) ... Setting up libncursesw5 (5.5-2ubuntu1) ... Setting up readline-common (5.1-7build1) ... Setting up libreadline5 (5.1-7build1) ... Setting up libssl0.9.8 (0.9.8b-2) ... Setting up mime-support (3.36-1) ... Setting up python2.4 (2.4.3-7ubuntu2) ... Setting up python (2.4.3-5ubuntu1) ... Setting up chrpath (0.13-2) ... Setting up html2text (1.3.2a-3) ... Setting up gettext (0.14.5-2ubuntu3) ... Setting up intltool-debian (0.34.2+20060621) ... Setting up po-debconf (1.0.5) ... Setting up debhelper (5.0.37.2ubuntu1) ... Setting up dpatch (2.0.20) ... Setting up libaspell15 (0.60.4-4) ... Setting up libaspell-dev (0.60.4-4) ... Setting up libglib2.0-0 (2.10.2-1ubuntu3) ... Setting up libatk1.0-0 (1.11.4-3) ... Setting up libglib2.0-dev (2.10.2-1ubuntu3) ... Setting up libatk1.0-dev (1.11.4-3) ... Setting up libpng12-0 (1.2.8rel-5.1) ... Setting up libpng12-dev (1.2.8rel-5.1) ... Setting up libjpeg62 (6b-13) ... Setting up libtiff4 (3.8.2-5) ... Setting up libxml2 (2.6.26.dfsg-2) ... Setting up libxml2-dev (2.6.26.dfsg-2) ... Setting up tcl8.4 (8.4.12-1) ... Setting up tk8.4 (8.4.12-1) ... Setting up ocaml-base-nox (3.09.2-5) ... Setting up ocaml-base (3.09.2-5) ... Setting up libncurses5-dev (5.5-2ubuntu1) ... Setting up ocaml-interp (3.09.2-5) ... Setting up ocaml-nox (3.09.2-5) ... Setting up ocaml (3.09.2-5) ... Setting up ocaml-native-compilers (3.09.2-5) ... Setting up libfontconfig1 (2.3.2-1.1ubuntu12) ... Setting up fontconfig (2.3.2-1.1ubuntu12) ... Creating config file /etc/fonts/local.conf with new version Updating font configuration of fontconfig... Cleaning up category cid.. Cleaning up category truetype.. Cleaning up category type1.. Updating category type1.. Updating category truetype.. Updating category cid.. Regenerating fonts cache... done. Setting up libxft2 (2.1.8.2-8) ... Setting up libfontconfig1-dev (2.3.2-1.1ubuntu12) ... Setting up libcairo2 (1.2.0-2) ... Setting up libpango1.0-common (1.13.2-1ubuntu1) ... Updating the modules list for Pango-1.5.0...done. Cleaning up font configuration of pango... Updating font configuration of pango... Cleaning up category xfont.. Updating category xfont.. *** You don't have any defomized font packages. *** So we are trying to force to generate pangox.aliases... Setting up libpango1.0-0 (1.13.2-1ubuntu1) ... Setting up libgtk2.0-common (2.10.0-0ubuntu1) ... Setting up libxext-dev (1.0.0-4build1) ... Setting up libgtk2.0-0 (2.8.17-1ubuntu5) ... Setting up libglade2-0 (2.5.1-2ubuntu2) ... Setting up libgtkspell0 (2.0.10-3) ... Setting up liblablgtk2-ocaml (2.6.0-7) ... Setting up libx11-dev (1.0.0-7ubuntu2) ... Setting up libxrender-dev (0.9.0.2-4build2) ... Setting up libxfixes-dev (3.0.1.2-4build1) ... Setting up libxcursor-dev (1.1.5.2-5ubuntu1) ... Setting up libxft-dev (2.1.8.2-8) ... Setting up libxi-dev (1.0.0-5ubuntu1) ... Setting up libxinerama-dev (1.0.1-4build1) ... Setting up libxrandr-dev (1.1.0.2-4ubuntu1) ... Setting up libcairo2-dev (1.2.0-2) ... Setting up libgtk2.0-bin (2.8.17-1ubuntu5) ... Updating the IM modules list for GTK+-2.4.0...done. Updating the gdk-pixbuf loaders list for GTK+-2.4.0...done. Setting up libpango1.0-dev (1.13.2-1ubuntu1) ... Setting up libgtk2.0-dev (2.8.17-1ubuntu5) ... Setting up libglade2-dev (2.5.1-2ubuntu2) ... Setting up libgtkspell-dev (2.0.10-3) ... Setting up liblablgtk2-ocaml-dev (2.6.0-7) ... Checking correctness of source dependencies... Toolchain package versions: libc6.1-dev_2.4-1ubuntu6 make_3.81-2 dpkg-dev_1.13.21ubuntu1 linux-kernel-headers_2.6.11.2-0ubuntu18 gcc-4.1_4.1.1-2ubuntu4 g++-4.1_4.1.1-2ubuntu4 binutils_2.17-1ubuntu1 libstdc++6-4.1-dev_4.1.1-2ubuntu4 libstdc++6_4.1.1-2ubuntu4 ------------------------------------------------------------------------------ dpkg-source: extracting coq in coq-8.0pl3 dpkg-source: unpacking coq_8.0pl3.orig.tar.gz dpkg-source: applying /srv/hooker.ubuntu.com/home/buildd/build-212105-157183/coq_8.0pl3-2.diff.gz dpkg-buildpackage: source package is coq dpkg-buildpackage: source version is 8.0pl3-2 dpkg-buildpackage: host architecture ia64 dpkg-buildpackage: source version without epoch 8.0pl3-2 /usr/bin/fakeroot debian/rules clean dpatch deapply-all coq-8.0pl3-ocaml-3.09 not applied to ./ . rm -rf patch-stamp patch-stampT debian/patched dh_testdir dh_testroot rm -f build-stamp configure-stamp opt-stamp /usr/bin/make clean make[1]: Entering directory `/build/buildd/coq-8.0pl3' Makefile:27: config/Makefile: No such file or directory make[1]: *** No rule to make target `config/Makefile'. Stop. make[1]: Leaving directory `/build/buildd/coq-8.0pl3' make: [clean] Error 2 (ignored) /usr/bin/make archclean make[1]: Entering directory `/build/buildd/coq-8.0pl3' Makefile:27: config/Makefile: No such file or directory make[1]: *** No rule to make target `config/Makefile'. Stop. make[1]: Leaving directory `/build/buildd/coq-8.0pl3' make: [clean] Error 2 (ignored) rm -f bin/parser.opt rm -f tools/coqdoc/*.cm[oi] rm -f config/coq_config.ml config/Makefile test-suite/check.log dh_clean debian/rules build test -d debian/patched || install -d debian/patched dpatch apply-all applying patch coq-8.0pl3-ocaml-3.09 to ./ ... ok. dpatch cat-all >>patch-stampT mv -f patch-stampT patch-stamp dh_testdir if [ -e /usr/bin/ocamlc.opt ]; \ then \ ./configure -opt --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all; \ else \ ./configure --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all; \ fi You have Objective-Caml 3.09.2. Good! You have native-code compilation. Good! LablGtk2 found, native threads: native CoqIde will be available Coq top directory : /build/buildd/coq-8.0pl3 Architecture : ia64 OS dependent libraries : -cclib -lunix Objective-Caml/Camlp4 version : 3.09.2 Objective-Caml/Camlp4 binaries in : /usr/bin Objective-Caml library in : /usr/lib/ocaml/3.09.2 Camlp4 library in : +camlp4 Reals theory : All CoqIde : opt Paths for true installation: binaries will be copied in /usr/bin library will be copied in /usr/lib/coq man pages will be copied in /usr/share/man emacs mode will be copied in /usr/share/emacs/site-lisp/coq If anything in the above is wrong, please restart './configure' *Warning* To compile the system for a new architecture don't forget to do a 'make archclean' before './configure'. touch configure-stamp dh_testdir if grep -q BEST=opt config/Makefile; \ then \ (/usr/bin/make check \ && touch opt-stamp) \ || (echo WARNING: NATIVE CODE COMPILATION FAILED \ && echo Trying to build coq in bytecode instead \ && /usr/bin/make archclean clean \ && /usr/bin/make BEST=byte HASCOQIDE=byte check \ && echo NATIVE CODE COMPILATION FAILED \ && echo Coq was built in bytecode instead); \ else \ /usr/bin/make BEST=byte HASCOQIDE=byte check; \ fi make[1]: Entering directory `/build/buildd/coq-8.0pl3' OCAMLC config/coq_config.mli OCAMLC config/coq_config.ml ECHO... > scripts/tolink.ml OCAMLC scripts/tolink.ml OCAMLC scripts/coqmktop.ml OCAMLC -o bin/coqmktop OCAMLOPT config/coq_config.ml OCAMLC lib/pp_control.mli OCAMLOPT lib/pp_control.ml OCAMLC lib/pp.mli OCAMLOPT4 lib/pp.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT lib/compat.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 lib/compat.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC lib/util.mli OCAMLOPT lib/util.ml OCAMLC lib/bignat.mli OCAMLOPT lib/bignat.ml OCAMLC lib/hashcons.mli OCAMLOPT lib/hashcons.ml OCAMLC lib/dyn.mli OCAMLOPT lib/dyn.ml OCAMLC lib/system.mli OCAMLOPT lib/system.ml OCAMLC lib/options.mli OCAMLOPT lib/options.ml OCAMLC lib/bstack.mli OCAMLOPT lib/bstack.ml OCAMLC lib/edit.mli OCAMLOPT lib/edit.ml OCAMLC lib/gset.mli OCAMLOPT lib/gset.ml OCAMLC lib/gmap.mli OCAMLOPT lib/gmap.ml OCAMLC lib/tlm.mli OCAMLOPT lib/tlm.ml OCAMLC lib/gmapl.mli OCAMLOPT lib/gmapl.ml OCAMLC lib/profile.mli OCAMLOPT lib/profile.ml OCAMLC lib/explore.mli OCAMLOPT lib/explore.ml OCAMLC lib/predicate.mli OCAMLOPT lib/predicate.ml OCAMLC lib/rtree.mli OCAMLOPT lib/rtree.ml OCAMLC lib/heap.mli OCAMLOPT lib/heap.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLC kernel/names.mli OCAMLOPT kernel/names.ml OCAMLC kernel/univ.mli OCAMLOPT kernel/univ.ml OCAMLC kernel/esubst.mli OCAMLOPT kernel/esubst.ml OCAMLC kernel/term.mli OCAMLOPT -rectypes kernel/term.ml OCAMLC kernel/sign.mli OCAMLOPT kernel/sign.ml OCAMLC kernel/declarations.mli OCAMLOPT kernel/declarations.ml OCAMLC kernel/environ.mli OCAMLOPT kernel/environ.ml OCAMLC kernel/closure.mli OCAMLOPT kernel/closure.ml OCAMLC kernel/conv_oracle.mli OCAMLOPT kernel/conv_oracle.ml OCAMLC kernel/reduction.mli OCAMLOPT kernel/reduction.ml OCAMLC kernel/entries.mli OCAMLOPT kernel/entries.ml OCAMLC kernel/modops.mli OCAMLOPT kernel/modops.ml OCAMLC kernel/type_errors.mli OCAMLOPT kernel/type_errors.ml OCAMLC kernel/inductive.mli OCAMLOPT kernel/inductive.ml OCAMLC kernel/typeops.mli OCAMLOPT kernel/typeops.ml File "kernel/typeops.ml", line 451, characters 5-59: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/indtypes.mli OCAMLOPT kernel/indtypes.ml OCAMLC kernel/cooking.mli OCAMLOPT kernel/cooking.ml OCAMLC kernel/term_typing.mli OCAMLOPT kernel/term_typing.ml File "kernel/term_typing.ml", line 34, characters 11-65: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/subtyping.mli OCAMLOPT kernel/subtyping.ml OCAMLC kernel/mod_typing.mli OCAMLOPT kernel/mod_typing.ml OCAMLC kernel/safe_typing.mli OCAMLOPT kernel/safe_typing.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLC library/nameops.mli OCAMLOPT library/nameops.ml OCAMLC library/libnames.mli OCAMLOPT library/libnames.ml OCAMLC library/libobject.mli OCAMLOPT library/libobject.ml OCAMLC library/summary.mli OCAMLOPT library/summary.ml OCAMLC library/nametab.mli OCAMLOPT -rectypes library/nametab.ml OCAMLC library/global.mli OCAMLOPT library/global.ml OCAMLC library/lib.mli OCAMLOPT library/lib.ml OCAMLC library/declaremods.mli OCAMLOPT library/declaremods.ml OCAMLC library/library.mli OCAMLOPT library/library.ml OCAMLC library/states.mli OCAMLOPT library/states.ml OCAMLOPT library/decl_kinds.ml OCAMLC library/dischargedhypsmap.mli OCAMLOPT library/dischargedhypsmap.ml OCAMLC library/goptions.mli OCAMLOPT library/goptions.ml OCAMLOPT -a -o library/library.cmxa OCAMLC pretyping/termops.mli OCAMLOPT pretyping/termops.ml OCAMLC pretyping/evd.mli OCAMLOPT pretyping/evd.ml OCAMLC pretyping/instantiate.mli OCAMLOPT pretyping/instantiate.ml OCAMLC pretyping/reductionops.mli OCAMLOPT pretyping/reductionops.ml OCAMLC pretyping/inductiveops.mli OCAMLOPT pretyping/inductiveops.ml OCAMLC pretyping/rawterm.mli OCAMLOPT pretyping/rawterm.ml OCAMLC pretyping/pattern.mli OCAMLOPT pretyping/pattern.ml OCAMLC pretyping/detyping.mli OCAMLOPT pretyping/detyping.ml OCAMLC pretyping/retyping.mli OCAMLOPT pretyping/retyping.ml OCAMLC pretyping/cbv.mli OCAMLOPT pretyping/cbv.ml OCAMLC pretyping/pretype_errors.mli OCAMLOPT pretyping/pretype_errors.ml OCAMLC pretyping/typing.mli OCAMLOPT pretyping/typing.ml OCAMLC pretyping/tacred.mli OCAMLOPT pretyping/tacred.ml OCAMLC library/decl_kinds.ml OCAMLC pretyping/classops.mli OCAMLOPT pretyping/classops.ml OCAMLC pretyping/recordops.mli OCAMLOPT pretyping/recordops.ml OCAMLC pretyping/indrec.mli OCAMLOPT pretyping/indrec.ml OCAMLC pretyping/evarutil.mli OCAMLOPT pretyping/evarutil.ml OCAMLC pretyping/evarconv.mli OCAMLOPT pretyping/evarconv.ml OCAMLC pretyping/coercion.mli OCAMLOPT pretyping/coercion.ml OCAMLC pretyping/cases.mli OCAMLOPT pretyping/cases.ml OCAMLC pretyping/pretyping.mli OCAMLOPT pretyping/pretyping.ml OCAMLC pretyping/matching.mli OCAMLOPT pretyping/matching.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLC parsing/lexer.mli OCAMLOPT4 parsing/lexer.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC interp/topconstr.mli OCAMLOPT interp/topconstr.ml OCAMLC interp/ppextend.mli OCAMLOPT interp/ppextend.ml OCAMLC interp/symbols.mli OCAMLOPT interp/symbols.ml OCAMLC interp/genarg.mli OCAMLOPT interp/genarg.ml OCAMLC interp/syntax_def.mli OCAMLOPT interp/syntax_def.ml OCAMLC interp/reserve.mli OCAMLOPT interp/reserve.ml OCAMLC library/impargs.mli OCAMLOPT library/impargs.ml OCAMLC parsing/coqast.mli OCAMLC interp/constrintern.mli OCAMLOPT interp/constrintern.ml OCAMLC interp/modintern.mli OCAMLOPT interp/modintern.ml OCAMLC interp/constrextern.mli OCAMLOPT interp/constrextern.ml OCAMLC interp/coqlib.mli OCAMLOPT interp/coqlib.ml OCAMLC library/declare.mli OCAMLOPT library/declare.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT parsing/coqast.ml OCAMLC parsing/ast.mli OCAMLOPT parsing/ast.ml OCAMLC parsing/termast.mli OCAMLOPT parsing/termast.ml OCAMLC parsing/extend.mli OCAMLOPT parsing/extend.ml OCAMLC parsing/esyntax.mli OCAMLOPT parsing/esyntax.ml OCAMLOPT -rectypes proofs/tacexpr.ml OCAMLC -rectypes proofs/tacexpr.ml OCAMLC toplevel/vernacexpr.ml OCAMLC parsing/pcoq.mli OCAMLOPT4 parsing/pcoq.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT toplevel/vernacexpr.ml OCAMLC translate/ppconstrnew.mli OCAMLOPT translate/ppconstrnew.ml OCAMLC parsing/ppconstr.mli OCAMLOPT parsing/ppconstr.ml OCAMLC parsing/printer.mli OCAMLOPT parsing/printer.ml OCAMLC proofs/proof_type.mli OCAMLC parsing/pptactic.mli OCAMLOPT parsing/pptactic.ml OCAMLC parsing/egrammar.mli OCAMLOPT parsing/egrammar.ml OCAMLC translate/pptacticnew.mli OCAMLOPT translate/pptacticnew.ml OCAMLC parsing/printmod.mli OCAMLOPT parsing/printmod.ml OCAMLC parsing/prettyp.mli OCAMLOPT parsing/prettyp.ml OCAMLC parsing/search.mli OCAMLOPT parsing/search.ml OCAMLOPT -a -o parsing/parsing.cmxa OCAMLOPT proofs/proof_type.ml OCAMLC proofs/proof_trees.mli OCAMLOPT proofs/proof_trees.ml OCAMLC proofs/logic.mli OCAMLOPT proofs/logic.ml OCAMLC proofs/refiner.mli OCAMLOPT proofs/refiner.ml OCAMLC proofs/evar_refiner.mli OCAMLOPT proofs/evar_refiner.ml OCAMLC proofs/tacmach.mli OCAMLOPT proofs/tacmach.ml OCAMLC proofs/clenv.mli OCAMLOPT proofs/clenv.ml OCAMLC proofs/pfedit.mli OCAMLOPT proofs/pfedit.ml OCAMLC proofs/tactic_debug.mli OCAMLOPT proofs/tactic_debug.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLC tactics/dn.mli OCAMLOPT tactics/dn.ml OCAMLC tactics/termdn.mli OCAMLOPT tactics/termdn.ml OCAMLC tactics/btermdn.mli OCAMLOPT tactics/btermdn.ml OCAMLC tactics/nbtermdn.mli OCAMLOPT tactics/nbtermdn.ml OCAMLC tactics/tacticals.mli OCAMLOPT tactics/tacticals.ml OCAMLC tactics/hipattern.mli OCAMLOPT tactics/hipattern.ml OCAMLC tactics/tactics.mli OCAMLOPT tactics/tactics.ml OCAMLC tactics/hiddentac.mli OCAMLOPT tactics/hiddentac.ml OCAMLC tactics/elim.mli OCAMLOPT tactics/elim.ml OCAMLC tactics/dhyp.mli OCAMLOPT tactics/dhyp.ml OCAMLC tactics/auto.mli OCAMLOPT tactics/auto.ml OCAMLC tactics/setoid_replace.mli OCAMLOPT tactics/setoid_replace.ml OCAMLC tactics/equality.mli OCAMLOPT tactics/equality.ml OCAMLC tactics/contradiction.mli OCAMLOPT tactics/contradiction.ml OCAMLC tactics/inv.mli OCAMLOPT tactics/inv.ml OCAMLC tactics/leminv.mli OCAMLOPT tactics/leminv.ml OCAMLC tactics/tacinterp.mli OCAMLOPT tactics/tacinterp.ml OCAMLOPT -a -o tactics/tactics.cmxa OCAMLC toplevel/himsg.mli OCAMLOPT toplevel/himsg.ml OCAMLC toplevel/cerrors.mli OCAMLOPT toplevel/cerrors.ml OCAMLC toplevel/class.mli OCAMLOPT toplevel/class.ml OCAMLC toplevel/metasyntax.mli OCAMLOPT toplevel/metasyntax.ml OCAMLC toplevel/command.mli OCAMLOPT toplevel/command.ml OCAMLC toplevel/record.mli OCAMLOPT toplevel/record.ml OCAMLC toplevel/recordobj.mli OCAMLOPT toplevel/recordobj.ml OCAMLC toplevel/discharge.mli OCAMLOPT toplevel/discharge.ml OCAMLC translate/ppvernacnew.mli OCAMLOPT translate/ppvernacnew.ml OCAMLC toplevel/vernacinterp.mli OCAMLOPT toplevel/vernacinterp.ml CAMLP4O toplevel/mltop.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC toplevel/mltop.mli OCAMLOPT toplevel/mltop.optml OCAMLC toplevel/vernacentries.mli OCAMLOPT toplevel/vernacentries.ml OCAMLC toplevel/vernac.mli OCAMLOPT toplevel/vernac.ml OCAMLC toplevel/line_oriented_parser.mli OCAMLOPT toplevel/line_oriented_parser.ml OCAMLC toplevel/protectedtoplevel.mli OCAMLOPT toplevel/protectedtoplevel.ml OCAMLC toplevel/toplevel.mli OCAMLOPT toplevel/toplevel.ml OCAMLC toplevel/usage.mli OCAMLOPT toplevel/usage.ml OCAMLC toplevel/coqinit.mli OCAMLOPT toplevel/coqinit.ml OCAMLC toplevel/coqtop.mli OCAMLOPT toplevel/coqtop.ml OCAMLOPT -a -o toplevel/toplevel.cmxa OCAMLOPT4 parsing/g_prim.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_proofs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_basevernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_vernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_tactic.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_ltac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_constr.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_cases.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_module.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/g_natsyntax.mli OCAMLOPT parsing/g_natsyntax.ml OCAMLC parsing/g_zsyntax.mli OCAMLOPT parsing/g_zsyntax.ml OCAMLOPT parsing/g_rsyntax.ml OCAMLOPT -a -o parsing/highparsing.cmxa OCAMLOPT4 parsing/g_primnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_constrnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_tacticnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_ltacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_vernacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 parsing/g_proofsnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o parsing/highparsingnew.cmxa OCAMLC tactics/autorewrite.mli OCAMLOPT tactics/autorewrite.ml OCAMLC tactics/refine.mli OCAMLOPT tactics/refine.ml OCAMLC tactics/extraargs.mli OCAMLC lib/pp_control.ml OCAMLC4 lib/pp.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC lib/util.ml OCAMLC lib/bignat.ml OCAMLC lib/dyn.ml OCAMLC lib/options.ml OCAMLC lib/hashcons.ml OCAMLC lib/predicate.ml OCAMLC lib/rtree.ml OCAMLC kernel/names.ml OCAMLC kernel/univ.ml OCAMLC kernel/esubst.ml OCAMLC -rectypes kernel/term.ml OCAMLC kernel/sign.ml OCAMLC kernel/declarations.ml OCAMLC kernel/environ.ml OCAMLC library/nameops.ml OCAMLC library/libnames.ml OCAMLC library/summary.ml OCAMLC -rectypes library/nametab.ml OCAMLC library/libobject.ml OCAMLC library/lib.ml OCAMLC library/goptions.ml OCAMLC pretyping/rawterm.ml OCAMLC pretyping/pattern.ml OCAMLC pretyping/evd.ml OCAMLC interp/topconstr.ml OCAMLC interp/genarg.ml OCAMLC interp/ppextend.ml OCAMLC parsing/coqast.ml OCAMLC parsing/ast.ml OCAMLC4 parsing/lexer.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/q_util.mli OCAMLC4 parsing/q_util.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/extend.ml OCAMLC4 parsing/pcoq.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/q_coqast.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/egrammar.ml OCAMLC4 parsing/argextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/tacextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/vernacextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_prim.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_tactic.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_ltac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_constr.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_primnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_tacticnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_ltacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_constrnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a parsing/grammar.cma OCAMLOPT4 tactics/extraargs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC tactics/extratactics.mli OCAMLOPT4 tactics/extratactics.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC tactics/eauto.mli OCAMLOPT4 tactics/eauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/tauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 tactics/eqdecide.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o tactics/hightactics.cmxa OCAMLOPT contrib/omega/omega.ml OCAMLOPT contrib/omega/coq_omega.ml OCAMLOPT4 contrib/omega/g_omega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/romega/omega2.ml OCAMLOPT contrib/romega/const_omega.ml OCAMLOPT contrib/romega/refl_omega.ml OCAMLOPT4 contrib/romega/g_romega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/ring/quote.ml OCAMLOPT4 contrib/ring/g_quote.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/ring/ring.ml OCAMLOPT4 contrib/ring/g_ring.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/field/field.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/fourier/fourier.ml OCAMLOPT contrib/fourier/fourierR.ml OCAMLOPT4 contrib/fourier/g_fourier.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/extraction/miniml.mli OCAMLC contrib/extraction/table.mli OCAMLOPT contrib/extraction/table.ml OCAMLC contrib/extraction/mlutil.mli OCAMLOPT contrib/extraction/mlutil.ml OCAMLC contrib/extraction/modutil.mli OCAMLOPT contrib/extraction/modutil.ml OCAMLC contrib/extraction/ocaml.mli OCAMLOPT contrib/extraction/ocaml.ml OCAMLC contrib/extraction/haskell.mli OCAMLOPT contrib/extraction/haskell.ml OCAMLC contrib/extraction/scheme.mli OCAMLOPT contrib/extraction/scheme.ml OCAMLC contrib/extraction/extraction.mli OCAMLOPT contrib/extraction/extraction.ml OCAMLC contrib/extraction/common.mli OCAMLOPT contrib/extraction/common.ml OCAMLC contrib/extraction/extract_env.mli OCAMLOPT contrib/extraction/extract_env.ml OCAMLOPT4 contrib/extraction/g_extraction.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/jprover/opname.mli OCAMLOPT contrib/jprover/opname.ml OCAMLC contrib/jprover/jterm.mli OCAMLOPT contrib/jprover/jterm.ml OCAMLC contrib/jprover/jlogic.mli OCAMLOPT contrib/jprover/jlogic.ml OCAMLC contrib/jprover/jtunify.mli OCAMLOPT contrib/jprover/jtunify.ml OCAMLC contrib/jprover/jall.mli OCAMLOPT contrib/jprover/jall.ml OCAMLOPT4 contrib/jprover/jprover.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/unshare.mli OCAMLOPT contrib/xml/unshare.ml OCAMLC contrib/xml/xml.mli OCAMLOPT4 contrib/xml/xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/xml/acic.ml OCAMLC contrib/xml/acic.ml OCAMLC contrib/xml/doubleTypeInference.mli OCAMLOPT contrib/xml/doubleTypeInference.ml OCAMLOPT contrib/xml/cic2acic.ml OCAMLOPT4 contrib/xml/acic2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT contrib/xml/proof2aproof.ml OCAMLC contrib/xml/proof2aproof.ml OCAMLC contrib/xml/xmlcommand.mli OCAMLOPT contrib/xml/xmlcommand.ml OCAMLOPT4 contrib/xml/proofTree2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT4 contrib/xml/xmlentries.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/cc/ccalgo.mli OCAMLOPT contrib/cc/ccalgo.ml OCAMLC contrib/cc/ccproof.mli OCAMLOPT contrib/cc/ccproof.ml OCAMLOPT4 contrib/cc/cctac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/funind/tacinvutils.mli OCAMLOPT contrib/funind/tacinvutils.ml OCAMLOPT4 contrib/funind/tacinv.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/first-order/formula.mli OCAMLOPT contrib/first-order/formula.ml OCAMLC contrib/first-order/unify.mli OCAMLOPT contrib/first-order/unify.ml OCAMLC contrib/first-order/sequent.mli OCAMLOPT contrib/first-order/sequent.ml OCAMLC contrib/first-order/rules.mli OCAMLOPT contrib/first-order/rules.ml OCAMLC contrib/first-order/instances.mli OCAMLOPT contrib/first-order/instances.ml OCAMLC contrib/first-order/ground.mli OCAMLOPT contrib/first-order/ground.ml OCAMLOPT4 contrib/first-order/g_ground.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLOPT -a -o contrib/contrib.cmxa COQMKTOP -o bin/coqtop.opt strip bin/coqtop.opt bin/coqtop.opt -boot -nois -compile theories/Init/Notations bin/coqtop.opt -boot -nois -compile theories/Init/Logic Defining 'IF' as keyword Defining 'exists2' as keyword bin/coqtop.opt -boot -nois -compile theories/Init/Datatypes bin/coqtop.opt -boot -nois -compile theories/Init/Peano bin/coqtop.opt -boot -nois -compile theories/Init/Specif bin/coqtop.opt -boot -nois -compile theories/Init/Logic_Type bin/coqtop.opt -boot -nois -compile theories/Init/Wf bin/coqtop.opt -boot -nois -compile theories/Init/Prelude bin/coqtop.opt -boot -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq bin/coqtop.opt -boot -compile theories/Logic/Hurkens bin/coqtop.opt -boot -compile theories/Logic/ProofIrrelevance bin/coqtop.opt -boot -compile theories/Logic/Classical_Prop bin/coqtop.opt -boot -compile theories/Logic/Classical_Pred_Type bin/coqtop.opt -boot -compile theories/Logic/Classical bin/coqtop.opt -boot -compile theories/Logic/Classical_Type bin/coqtop.opt -boot -compile theories/Logic/Classical_Pred_Set bin/coqtop.opt -boot -compile theories/Logic/Eqdep bin/coqtop.opt -boot -compile theories/Logic/ClassicalFacts bin/coqtop.opt -boot -compile theories/Logic/ChoiceFacts bin/coqtop.opt -boot -compile theories/Logic/Berardi bin/coqtop.opt -boot -compile theories/Logic/Eqdep_dec bin/coqtop.opt -boot -compile theories/Logic/Decidable bin/coqtop.opt -boot -compile theories/Logic/JMeq bin/coqtop.opt -boot -compile theories/Logic/ClassicalDescription bin/coqtop.opt -boot -compile theories/Logic/RelationalChoice bin/coqtop.opt -boot -compile theories/Logic/ClassicalChoice bin/coqtop.opt -boot -compile theories/Bool/Bool bin/coqtop.opt -boot -compile theories/Logic/Diaconescu bin/coqtop.opt -boot -compile theories/Arith/Le bin/coqtop.opt -boot -compile theories/Arith/Lt bin/coqtop.opt -boot -compile theories/Arith/Plus bin/coqtop.opt -boot -compile theories/Arith/Gt bin/coqtop.opt -boot -compile theories/Arith/Minus bin/coqtop.opt -boot -compile theories/Arith/Mult bin/coqtop.opt -boot -compile theories/Arith/Between bin/coqtop.opt -boot -compile theories/Arith/Peano_dec bin/coqtop.opt -boot -compile theories/Arith/Compare_dec bin/coqtop.opt -boot -compile theories/Arith/Factorial bin/coqtop.opt -boot -compile theories/Arith/Arith bin/coqtop.opt -boot -compile theories/Arith/Wf_nat bin/coqtop.opt -boot -compile theories/Arith/Min bin/coqtop.opt -boot -compile theories/Arith/Compare bin/coqtop.opt -boot -compile theories/Arith/Even bin/coqtop.opt -boot -compile theories/Arith/Div2 bin/coqtop.opt -boot -compile theories/Arith/EqNat bin/coqtop.opt -boot -compile theories/Arith/Euclid bin/coqtop.opt -boot -compile theories/Arith/Max bin/coqtop.opt -boot -compile theories/Bool/Sumbool bin/coqtop.opt -boot -compile theories/Arith/Bool_nat bin/coqtop.opt -boot -compile theories/Bool/IfProp bin/coqtop.opt -boot -compile theories/Bool/Zerob bin/coqtop.opt -boot -compile theories/Bool/DecBool bin/coqtop.opt -boot -compile theories/Bool/BoolEq bin/coqtop.opt -boot -compile theories/Bool/Bvector bin/coqtop.opt -boot -compile theories/NArith/BinPos bin/coqtop.opt -boot -compile theories/NArith/Pnat bin/coqtop.opt -boot -compile theories/NArith/BinNat bin/coqtop.opt -boot -compile theories/NArith/NArith bin/coqtop.opt -boot -compile theories/ZArith/BinInt bin/coqtop.opt -boot -compile theories/ZArith/Zcompare bin/coqtop.opt -boot -compile theories/ZArith/Zorder bin/coqtop.opt -boot -compile theories/ZArith/Znat bin/coqtop.opt -boot -compile theories/ZArith/Zmisc bin/coqtop.opt -boot -compile theories/ZArith/Wf_Z bin/coqtop.opt -boot -compile theories/ZArith/Zeven bin/coqtop.opt -boot -compile theories/ZArith/Zmin bin/coqtop.opt -boot -compile theories/ZArith/ZArith_dec bin/coqtop.opt -boot -compile theories/ZArith/Zabs bin/coqtop.opt -boot -compile theories/ZArith/auxiliary bin/coqtop.opt -boot -compile theories/ZArith/Zbool bin/coqtop.opt -boot -compile theories/ZArith/Zhints bin/coqtop.opt -boot -compile theories/ZArith/ZArith_base bin/coqtop.opt -boot -compile contrib/ring/Ring_theory bin/coqtop.opt -boot -compile contrib/ring/Quote bin/coqtop.opt -boot -compile contrib/ring/Ring_normalize bin/coqtop.opt -boot -compile contrib/ring/Ring_abstract bin/coqtop.opt -boot -compile contrib/ring/Ring bin/coqtop.opt -boot -compile contrib/ring/ArithRing bin/coqtop.opt -boot -compile contrib/ring/ZArithRing bin/coqtop.opt -boot -compile contrib/omega/OmegaLemmas bin/coqtop.opt -boot -compile contrib/omega/Omega bin/coqtop.opt -boot -compile theories/Lists/List bin/coqtop.opt -boot -compile theories/ZArith/Zcomplements bin/coqtop.opt -boot -compile theories/ZArith/Zsqrt bin/coqtop.opt -boot -compile theories/ZArith/Zpower bin/coqtop.opt -boot -compile theories/ZArith/Zdiv Defining 'mod' as keyword bin/coqtop.opt -boot -compile theories/ZArith/Zlogarithm bin/coqtop.opt -boot -compile theories/ZArith/ZArith bin/coqtop.opt -boot -compile theories/ZArith/Zwf bin/coqtop.opt -boot -compile theories/ZArith/Zbinary bin/coqtop.opt -boot -compile theories/ZArith/Znumtheory bin/coqtop.opt -boot -compile theories/Lists/MonoList bin/coqtop.opt -boot -compile theories/Lists/ListSet bin/coqtop.opt -boot -compile theories/Lists/Streams bin/coqtop.opt -boot -compile theories/Lists/TheoryList bin/coqtop.opt -boot -compile theories/Sets/Ensembles bin/coqtop.opt -boot -compile theories/Sets/Constructive_sets bin/coqtop.opt -boot -compile theories/Sets/Classical_sets bin/coqtop.opt -boot -compile theories/Sets/Permut bin/coqtop.opt -boot -compile theories/Sets/Relations_1 bin/coqtop.opt -boot -compile theories/Sets/Relations_1_facts bin/coqtop.opt -boot -compile theories/Sets/Partial_Order bin/coqtop.opt -boot -compile theories/Sets/Cpo bin/coqtop.opt -boot -compile theories/Sets/Powerset bin/coqtop.opt -boot -compile theories/Sets/Powerset_facts bin/coqtop.opt -boot -compile theories/Sets/Powerset_Classical_facts bin/coqtop.opt -boot -compile theories/Sets/Finite_sets bin/coqtop.opt -boot -compile theories/Sets/Finite_sets_facts bin/coqtop.opt -boot -compile theories/Sets/Image bin/coqtop.opt -boot -compile theories/Sets/Relations_2 bin/coqtop.opt -boot -compile theories/Sets/Infinite_sets bin/coqtop.opt -boot -compile theories/Sets/Relations_2_facts bin/coqtop.opt -boot -compile theories/Sets/Integers bin/coqtop.opt -boot -compile theories/Sets/Relations_3 bin/coqtop.opt -boot -compile theories/Sets/Multiset bin/coqtop.opt -boot -compile theories/Sets/Relations_3_facts bin/coqtop.opt -boot -compile theories/Sets/Uniset bin/coqtop.opt -boot -compile theories/IntMap/Addr bin/coqtop.opt -boot -compile theories/IntMap/Adist bin/coqtop.opt -boot -compile theories/IntMap/Addec bin/coqtop.opt -boot -compile theories/IntMap/Map bin/coqtop.opt -boot -compile theories/IntMap/Fset bin/coqtop.opt -boot -compile theories/IntMap/Adalloc bin/coqtop.opt -boot -compile theories/IntMap/Mapaxioms bin/coqtop.opt -boot -compile theories/IntMap/Mapiter bin/coqtop.opt -boot -compile theories/IntMap/Lsort bin/coqtop.opt -boot -compile theories/IntMap/Mapsubset bin/coqtop.opt -boot -compile theories/IntMap/Mapcard bin/coqtop.opt -boot -compile theories/IntMap/Mapcanon bin/coqtop.opt -boot -compile theories/IntMap/Mapc bin/coqtop.opt -boot -compile theories/IntMap/Mapfold bin/coqtop.opt -boot -compile theories/IntMap/Maplists bin/coqtop.opt -boot -compile theories/IntMap/Allmaps bin/coqtop.opt -boot -compile theories/Relations/Rstar bin/coqtop.opt -boot -compile theories/Relations/Newman bin/coqtop.opt -boot -compile theories/Relations/Relation_Definitions bin/coqtop.opt -boot -compile theories/Relations/Relation_Operators bin/coqtop.opt -boot -compile theories/Relations/Operators_Properties bin/coqtop.opt -boot -compile theories/Relations/Relations bin/coqtop.opt -boot -compile theories/Wellfounded/Disjoint_Union bin/coqtop.opt -boot -compile theories/Wellfounded/Inclusion bin/coqtop.opt -boot -compile theories/Wellfounded/Inverse_Image bin/coqtop.opt -boot -compile theories/Wellfounded/Transitive_Closure bin/coqtop.opt -boot -compile theories/Wellfounded/Lexicographic_Exponentiation bin/coqtop.opt -boot -compile theories/Wellfounded/Union bin/coqtop.opt -boot -compile theories/Wellfounded/Lexicographic_Product bin/coqtop.opt -boot -compile theories/Wellfounded/Well_Ordering bin/coqtop.opt -boot -compile theories/Wellfounded/Wellfounded bin/coqtop.opt -boot -compile theories/Reals/Rdefinitions bin/coqtop.opt -boot -compile theories/Reals/Raxioms bin/coqtop.opt -boot -compile contrib/field/Field_Compl bin/coqtop.opt -boot -compile contrib/field/Field_Theory bin/coqtop.opt -boot -compile contrib/field/Field_Tactic bin/coqtop.opt -boot -compile contrib/field/Field bin/coqtop.opt -boot -compile theories/Reals/RIneq bin/coqtop.opt -boot -compile theories/Reals/DiscrR bin/coqtop.opt -boot -compile theories/Reals/Rbase bin/coqtop.opt -boot -compile theories/Reals/R_Ifp OCAMLC contrib/ring/quote.ml OCAMLC contrib/ring/ring.ml OCAMLC contrib/fourier/fourier.ml OCAMLC contrib/fourier/fourierR.ml OCAMLC4 contrib/field/field.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. bin/coqtop.opt -boot -compile contrib/fourier/Fourier_util bin/coqtop.opt -boot -compile contrib/fourier/Fourier bin/coqtop.opt -boot -compile theories/Reals/Rbasic_fun bin/coqtop.opt -boot -compile theories/Reals/R_sqr bin/coqtop.opt -boot -compile theories/Reals/SplitAbsolu bin/coqtop.opt -boot -compile theories/Reals/SplitRmult bin/coqtop.opt -boot -compile theories/Reals/ArithProp bin/coqtop.opt -boot -compile theories/Reals/Rfunctions bin/coqtop.opt -boot -compile theories/Reals/Rseries bin/coqtop.opt -boot -compile theories/Reals/SeqProp bin/coqtop.opt -boot -compile theories/Reals/Rcomplete bin/coqtop.opt -boot -compile theories/Reals/PartSum bin/coqtop.opt -boot -compile theories/Reals/AltSeries bin/coqtop.opt -boot -compile theories/Reals/Binomial bin/coqtop.opt -boot -compile theories/Reals/Rsigma bin/coqtop.opt -boot -compile theories/Reals/Rprod bin/coqtop.opt -boot -compile theories/Reals/Cauchy_prod bin/coqtop.opt -boot -compile theories/Reals/Alembert bin/coqtop.opt -boot -compile theories/Reals/SeqSeries bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_fun bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_def bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_alt bin/coqtop.opt -boot -compile theories/Reals/Cos_rel bin/coqtop.opt -boot -compile theories/Reals/Cos_plus bin/coqtop.opt -boot -compile theories/Reals/Rtrigo bin/coqtop.opt -boot -compile theories/Reals/Rlimit bin/coqtop.opt -boot -compile theories/Reals/Rderiv bin/coqtop.opt -boot -compile theories/Reals/RList bin/coqtop.opt -boot -compile theories/Reals/Ranalysis1 Defining 'o' as keyword bin/coqtop.opt -boot -compile theories/Reals/Ranalysis2 bin/coqtop.opt -boot -compile theories/Reals/Ranalysis3 bin/coqtop.opt -boot -compile theories/Reals/Rtopology bin/coqtop.opt -boot -compile theories/Reals/MVT bin/coqtop.opt -boot -compile theories/Reals/PSeries_reg bin/coqtop.opt -boot -compile theories/Reals/Exp_prop bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_reg bin/coqtop.opt -boot -compile theories/Reals/Rsqrt_def bin/coqtop.opt -boot -compile theories/Reals/R_sqrt bin/coqtop.opt -boot -compile theories/Reals/Rtrigo_calc bin/coqtop.opt -boot -compile theories/Reals/Rgeom bin/coqtop.opt -boot -compile theories/Reals/Sqrt_reg bin/coqtop.opt -boot -compile theories/Reals/Ranalysis4 bin/coqtop.opt -boot -compile theories/Reals/Rpower bin/coqtop.opt -boot -compile theories/Reals/Ranalysis bin/coqtop.opt -boot -compile theories/Reals/NewtonInt bin/coqtop.opt -boot -compile theories/Reals/RiemannInt_SF bin/coqtop.opt -boot -compile theories/Reals/RiemannInt bin/coqtop.opt -boot -compile theories/Reals/Integration bin/coqtop.opt -boot -compile theories/Reals/Reals bin/coqtop.opt -boot -compile theories/Setoids/Setoid bin/coqtop.opt -boot -compile theories/Sorting/Permutation bin/coqtop.opt -boot -compile theories/Sorting/Sorting bin/coqtop.opt -boot -compile theories/Sorting/Heap bin/coqtop.opt -boot -compile contrib/romega/ReflOmegaCore Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable bin/coqtop.opt -boot -compile contrib/romega/ROmega bin/coqtop.opt -boot -compile contrib/ring/NArithRing bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring_theory bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring_normalize bin/coqtop.opt -boot -compile contrib/ring/Setoid_ring bin/coqtop.opt -boot -compile contrib/cc/CCSolve OCAMLLEX tools/coqdep_lexer.mll 187 states, 5170 transitions, table size 21802 bytes OCAMLC tools/coqdep_lexer.ml OCAMLC tools/coqdep.ml OCAMLC -o bin/coqdep OCAMLC4 tools/coq_makefile.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -o bin/coq_makefile OCAMLLEX tools/gallina_lexer.mll 151 states, 498 transitions, table size 2898 bytes OCAMLC tools/gallina_lexer.ml OCAMLC tools/gallina.ml File "tools/gallina.ml", line 25, characters 20-44: Warning X: this statement never returns (or has an unsound type.) File "tools/gallina.ml", line 38, characters 20-44: Warning X: this statement never returns (or has an unsound type.) OCAMLC -o bin/gallina OCAMLC4 tools/coq-tex.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -o bin/coq-tex OCAMLLEX tools/coqwc.mll 148 states, 742 transitions, table size 3856 bytes OCAMLC tools/coqwc.ml OCAMLC -o bin/coqwc OCAMLC tools/coqdoc/alpha.mli OCAMLC tools/coqdoc/alpha.ml OCAMLC tools/coqdoc/index.mli OCAMLLEX tools/coqdoc/index.mll 166 states, 4253 transitions, table size 18008 bytes OCAMLC tools/coqdoc/index.ml OCAMLC tools/coqdoc/output.mli OCAMLC tools/coqdoc/output.ml OCAMLC tools/coqdoc/pretty.mli OCAMLLEX tools/coqdoc/pretty.mll 477 states, 19341 transitions, table size 80226 bytes OCAMLC tools/coqdoc/pretty.ml OCAMLC tools/coqdoc/main.ml OCAMLC -o bin/coqdoc OCAMLC dev/top_printers.ml OCAMLC toplevel/usage.ml OCAMLC scripts/coqc.ml OCAMLC lib/system.ml OCAMLC lib/bstack.ml OCAMLC lib/edit.ml OCAMLC lib/gset.ml OCAMLC lib/gmap.ml OCAMLC lib/tlm.ml OCAMLC lib/gmapl.ml OCAMLC lib/profile.ml OCAMLC lib/explore.ml OCAMLC lib/heap.ml OCAMLC -a -o lib/lib.cma OCAMLC kernel/closure.ml OCAMLC kernel/conv_oracle.ml OCAMLC kernel/reduction.ml OCAMLC kernel/entries.ml OCAMLC kernel/modops.ml OCAMLC kernel/type_errors.ml OCAMLC kernel/inductive.ml OCAMLC kernel/typeops.ml File "kernel/typeops.ml", line 451, characters 5-59: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/indtypes.ml OCAMLC kernel/cooking.ml OCAMLC kernel/term_typing.ml File "kernel/term_typing.ml", line 34, characters 11-65: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/subtyping.ml OCAMLC kernel/mod_typing.ml OCAMLC kernel/safe_typing.ml OCAMLC -a -o kernel/kernel.cma OCAMLC library/global.ml OCAMLC library/declaremods.ml OCAMLC library/library.ml OCAMLC library/states.ml OCAMLC library/dischargedhypsmap.ml OCAMLC -a -o library/library.cma OCAMLC pretyping/termops.ml OCAMLC pretyping/instantiate.ml OCAMLC pretyping/reductionops.ml OCAMLC pretyping/inductiveops.ml OCAMLC pretyping/detyping.ml OCAMLC pretyping/retyping.ml OCAMLC pretyping/cbv.ml OCAMLC pretyping/pretype_errors.ml OCAMLC pretyping/typing.ml OCAMLC pretyping/tacred.ml OCAMLC pretyping/classops.ml OCAMLC pretyping/recordops.ml OCAMLC pretyping/indrec.ml OCAMLC pretyping/evarutil.ml OCAMLC pretyping/evarconv.ml OCAMLC pretyping/coercion.ml OCAMLC pretyping/cases.ml OCAMLC pretyping/pretyping.ml OCAMLC pretyping/matching.ml OCAMLC -a -o pretyping/pretyping.cma OCAMLC interp/symbols.ml OCAMLC interp/syntax_def.ml OCAMLC interp/reserve.ml OCAMLC library/impargs.ml OCAMLC interp/constrintern.ml OCAMLC interp/modintern.ml OCAMLC interp/constrextern.ml OCAMLC interp/coqlib.ml OCAMLC library/declare.ml OCAMLC -a -o interp/interp.cma OCAMLC parsing/termast.ml OCAMLC parsing/esyntax.ml OCAMLC parsing/ppconstr.ml OCAMLC translate/ppconstrnew.ml OCAMLC parsing/printer.ml OCAMLC parsing/pptactic.ml OCAMLC translate/pptacticnew.ml OCAMLC parsing/printmod.ml OCAMLC parsing/prettyp.ml OCAMLC parsing/search.ml OCAMLC -a -o parsing/parsing.cma OCAMLC proofs/proof_type.ml OCAMLC proofs/proof_trees.ml OCAMLC proofs/logic.ml OCAMLC proofs/refiner.ml OCAMLC proofs/evar_refiner.ml OCAMLC proofs/tacmach.ml OCAMLC proofs/clenv.ml OCAMLC proofs/pfedit.ml OCAMLC proofs/tactic_debug.ml OCAMLC -a -o proofs/proofs.cma OCAMLC tactics/dn.ml OCAMLC tactics/termdn.ml OCAMLC tactics/btermdn.ml OCAMLC tactics/nbtermdn.ml OCAMLC tactics/tacticals.ml OCAMLC tactics/hipattern.ml OCAMLC tactics/tactics.ml OCAMLC tactics/hiddentac.ml OCAMLC tactics/elim.ml OCAMLC tactics/dhyp.ml OCAMLC tactics/auto.ml OCAMLC tactics/setoid_replace.ml OCAMLC tactics/equality.ml OCAMLC tactics/contradiction.ml OCAMLC tactics/inv.ml OCAMLC tactics/leminv.ml OCAMLC tactics/tacinterp.ml OCAMLC -a -o tactics/tactics.cma OCAMLC toplevel/himsg.ml OCAMLC toplevel/cerrors.ml OCAMLC toplevel/class.ml OCAMLC toplevel/metasyntax.ml OCAMLC toplevel/command.ml OCAMLC toplevel/record.ml OCAMLC toplevel/recordobj.ml OCAMLC toplevel/discharge.ml OCAMLC translate/ppvernacnew.ml OCAMLC toplevel/vernacinterp.ml CAMLP4O toplevel/mltop.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC toplevel/mltop.byteml OCAMLC toplevel/vernacentries.ml OCAMLC toplevel/vernac.ml OCAMLC toplevel/line_oriented_parser.ml OCAMLC toplevel/protectedtoplevel.ml OCAMLC toplevel/toplevel.ml OCAMLC toplevel/coqinit.ml OCAMLC toplevel/coqtop.ml OCAMLC -a -o toplevel/toplevel.cma OCAMLC4 parsing/g_proofs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_basevernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_vernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_cases.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_module.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/g_natsyntax.ml OCAMLC parsing/g_zsyntax.ml OCAMLC parsing/g_rsyntax.ml OCAMLC -a -o parsing/highparsing.cma OCAMLC4 parsing/g_vernacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_proofsnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o parsing/highparsingnew.cma OCAMLC tactics/autorewrite.ml OCAMLC tactics/refine.ml OCAMLC4 tactics/extraargs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/extratactics.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/eauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/tauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/eqdecide.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o tactics/hightactics.cma OCAMLC contrib/omega/omega.ml OCAMLC contrib/omega/coq_omega.ml OCAMLC4 contrib/omega/g_omega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/romega/omega2.ml OCAMLC contrib/romega/const_omega.ml OCAMLC contrib/romega/refl_omega.ml OCAMLC4 contrib/romega/g_romega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/ring/g_quote.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/ring/g_ring.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/fourier/g_fourier.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/extraction/table.ml OCAMLC contrib/extraction/mlutil.ml OCAMLC contrib/extraction/modutil.ml OCAMLC contrib/extraction/ocaml.ml OCAMLC contrib/extraction/haskell.ml OCAMLC contrib/extraction/scheme.ml OCAMLC contrib/extraction/extraction.ml OCAMLC contrib/extraction/common.ml OCAMLC contrib/extraction/extract_env.ml OCAMLC4 contrib/extraction/g_extraction.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/jprover/opname.ml OCAMLC contrib/jprover/jterm.ml OCAMLC contrib/jprover/jlogic.ml OCAMLC contrib/jprover/jtunify.ml OCAMLC contrib/jprover/jall.ml OCAMLC4 contrib/jprover/jprover.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/unshare.ml OCAMLC4 contrib/xml/xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/doubleTypeInference.ml OCAMLC contrib/xml/cic2acic.ml OCAMLC4 contrib/xml/acic2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/xmlcommand.ml OCAMLC4 contrib/xml/proofTree2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/xml/xmlentries.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/cc/ccalgo.ml OCAMLC contrib/cc/ccproof.ml OCAMLC4 contrib/cc/cctac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/funind/tacinvutils.ml OCAMLC4 contrib/funind/tacinv.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/first-order/formula.ml OCAMLC contrib/first-order/unify.ml OCAMLC contrib/first-order/sequent.ml OCAMLC contrib/first-order/rules.ml OCAMLC contrib/first-order/instances.ml OCAMLC contrib/first-order/ground.ml OCAMLC4 contrib/first-order/g_ground.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o contrib/contrib.cma COQMKTOP -o bin/coqtop.byte OCAMLC -o bin/coqc cd bin; ln -sf coqtop.opt coqtop bin/coqtop.opt -boot -translate -strict-implicit -nois -compile theories7/Init/Notations make[1]: *** [theories7/Init/Notations.vo] Segmentation fault make[1]: Leaving directory `/build/buildd/coq-8.0pl3' WARNING: NATIVE CODE COMPILATION FAILED Trying to build coq in bytecode instead make[1]: Entering directory `/build/buildd/coq-8.0pl3' rm -f contrib/*/*.cmx contrib/*.cmxa contrib/*.a contrib/*/*.[so] rm -f bin/* rm -f config/*.cmx* config/*.[soa] rm -f lib/*.cmx* lib/*.[soa] rm -f kernel/*.cmx* kernel/*.[soa] rm -f library/*.cmx* library/*.[soa] rm -f proofs/*.cmx* proofs/*.[soa] rm -f tactics/*.cmx* tactics/*.[soa] rm -f interp/*.cmx* interp/*.[soa] rm -f parsing/*.cmx* parsing/*.[soa] rm -f pretyping/*.cmx* pretyping/*.[soa] rm -f toplevel/*.cmx* toplevel/*.[soa] rm -f ide/*.cmx* ide/*.[soa] rm -f ide/utils/*.cmx* ide/utils/*.[soa] rm -f translate/*.cmx* translate/*.[soa] rm -f tools/*.cmx* tools/*.[soa] rm -f tools/*/*.cmx* tools/*/*.[soa] rm -f scripts/*.cmx* scripts/*.[soa] rm -f dev/*.cmx* dev/*.[soa] rm -f scripts/tolink.ml rm -f ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml rm -f ide/utf8.vo ide/utils/okey.cmo ide/utils/uoptions.cmo ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo ide/utils/configwin_ihm.cmo ide/utils/configwin.cmo ide/utils/editable_cells.cmo ide/config_parser.cmo ide/config_lexer.cmo ide/utf8_convert.cmo ide/preferences.cmo ide/ideutils.cmo ide/blaster_window.cmo ide/undo.cmo ide/find_phrase.cmo ide/highlight.cmo ide/coq.cmo ide/coq_commands.cmo ide/coq_tactics.cmo ide/command_windows.cmo ide/coqide.cmo ide/utils/okey.cmx ide/utils/uoptions.cmx ide/utils/configwin_keys.cmx ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx ide/utils/configwin_ihm.cmx ide/utils/configwin.cmx ide/utils/editable_cells.cmx ide/config_parser.cmx ide/config_lexer.cmx ide/utf8_convert.cmx ide/preferences.cmx ide/ideutils.cmx ide/blaster_window.cmx ide/undo.cmx ide/find_phrase.cmx ide/highlight.cmx ide/coq.cmx ide/coq_commands.cmx ide/coq_tactics.cmx ide/command_windows.cmx ide/coqide.cmx ide/utils/okey.cmi ide/utils/uoptions.cmi ide/utils/configwin_keys.cmi ide/utils/configwin_types.cmi ide/utils/configwin_messages.cmi ide/utils/configwin_ihm.cmi ide/utils/configwin.cmi ide/utils/editable_cells.cmi ide/config_parser.cmi ide/config_lexer.cmi ide/utf8_convert.cmi ide/preferences.cmi ide/ideutils.cmi ide/blaster_window.cmi ide/undo.cmi ide/find_phrase.cmi ide/highlight.cmi ide/coq.cmi ide/coq_commands.cmi ide/coq_tactics.cmi ide/command_windows.cmi ide/coqide.cmi rm -f bin/coqide.byte bin/coqide.opt bin/coqide rm -f states/*.coq states7/*.coq rm -f theories/*/*.vo theories7/*/*.vo rm -f contrib/*/*.cm[io] contrib/*.cma contrib/*/*.vo contrib7/*/*.vo rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml rm -f tools/coqwc.ml rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml rm -f doc/coq.tex rm -f parsing/grammar.cma rm -f toplevel/mltop.byteml toplevel/mltop.optml rm -f *~ */*~ */*/*~ rm -f gmon.out core rm -f config/*.cm[ioa] rm -f lib/*.cm[ioa] rm -f kernel/*.cm[ioa] rm -f library/*.cm[ioa] rm -f proofs/*.cm[ioa] rm -f tactics/*.cm[ioa] rm -f interp/*.cm[ioa] rm -f parsing/*.cm[ioa] parsing/*.ppo rm -f pretyping/*.cm[ioa] rm -f toplevel/*.cm[ioa] rm -f ide/*.cm[ioa] rm -f ide/utils/*.cm[ioa] rm -f translate/*.cm[ioa] rm -f tools/*.cm[ioa] rm -f tools/*/*.cm[ioa] rm -f scripts/*.cm[ioa] rm -f dev/*.cm[ioa] rm -f */*.pp[iox] contrib/*/*.pp[iox] rm -f tactics/tauto.ml tactics/eqdecide.ml tactics/extraargs.ml tactics/extratactics.ml tactics/eauto.ml contrib/omega/g_omega.ml contrib/romega/g_romega.ml contrib/ring/g_quote.ml contrib/ring/g_ring.ml contrib/field/field.ml contrib/fourier/g_fourier.ml contrib/extraction/g_extraction.ml contrib/xml/xmlentries.ml contrib/jprover/jprover.ml contrib/cc/cctac.ml contrib/funind/tacinv.ml contrib/first-order/g_ground.ml contrib/interface/debug_tac.ml contrib/interface/centaur.ml parsing/lexer.ml parsing/q_util.ml parsing/q_coqast.ml parsing/g_prim.ml parsing/pcoq.ml parsing/g_basevernac.ml parsing/g_minicoq.ml parsing/g_vernac.ml parsing/g_proofs.ml parsing/g_cases.ml parsing/g_constr.ml parsing/g_module.ml parsing/g_tactic.ml parsing/g_ltac.ml parsing/argextend.ml parsing/tacextend.ml parsing/vernacextend.ml parsing/g_primnew.ml parsing/g_vernacnew.ml parsing/g_proofsnew.ml parsing/g_constrnew.ml parsing/g_tacticnew.ml parsing/g_ltacnew.ml toplevel/mltop.ml lib/pp.ml lib/compat.ml contrib/xml/xml.ml contrib/xml/acic2Xml.ml contrib/xml/proofTree2Xml.ml contrib/interface/line_parser.ml tools/coq_makefile.ml tools/coq-tex.ml rm -fr *.v8 syntax/*.v8 ide/*.v8 theories7/*/*.v8 contrib7/*/*.v8 find . -name "\.#*" -exec rm -f {} \; find . -name "*~" -exec rm -f {} \; make[1]: Leaving directory `/build/buildd/coq-8.0pl3' make[1]: Entering directory `/build/buildd/coq-8.0pl3' OCAMLC config/coq_config.mli OCAMLC config/coq_config.ml ECHO... > scripts/tolink.ml OCAMLC scripts/tolink.ml OCAMLC scripts/coqmktop.ml OCAMLC -o bin/coqmktop OCAMLC lib/pp_control.mli OCAMLC lib/pp_control.ml OCAMLC lib/pp.mli OCAMLC4 lib/pp.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 lib/compat.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC lib/util.mli OCAMLC lib/util.ml OCAMLC lib/bignat.mli OCAMLC lib/bignat.ml OCAMLC lib/hashcons.mli OCAMLC lib/hashcons.ml OCAMLC lib/dyn.mli OCAMLC lib/dyn.ml OCAMLC lib/system.mli OCAMLC lib/system.ml OCAMLC lib/options.mli OCAMLC lib/options.ml OCAMLC lib/bstack.mli OCAMLC lib/bstack.ml OCAMLC lib/edit.mli OCAMLC lib/edit.ml OCAMLC lib/gset.mli OCAMLC lib/gset.ml OCAMLC lib/gmap.mli OCAMLC lib/gmap.ml OCAMLC lib/tlm.mli OCAMLC lib/tlm.ml OCAMLC lib/gmapl.mli OCAMLC lib/gmapl.ml OCAMLC lib/profile.mli OCAMLC lib/profile.ml OCAMLC lib/explore.mli OCAMLC lib/explore.ml OCAMLC lib/predicate.mli OCAMLC lib/predicate.ml OCAMLC lib/rtree.mli OCAMLC lib/rtree.ml OCAMLC lib/heap.mli OCAMLC lib/heap.ml OCAMLC -a -o lib/lib.cma OCAMLC kernel/names.mli OCAMLC kernel/names.ml OCAMLC kernel/univ.mli OCAMLC kernel/univ.ml OCAMLC kernel/esubst.mli OCAMLC kernel/esubst.ml OCAMLC kernel/term.mli OCAMLC -rectypes kernel/term.ml OCAMLC kernel/sign.mli OCAMLC kernel/sign.ml OCAMLC kernel/declarations.mli OCAMLC kernel/declarations.ml OCAMLC kernel/environ.mli OCAMLC kernel/environ.ml OCAMLC kernel/closure.mli OCAMLC kernel/closure.ml OCAMLC kernel/conv_oracle.mli OCAMLC kernel/conv_oracle.ml OCAMLC kernel/reduction.mli OCAMLC kernel/reduction.ml OCAMLC kernel/entries.mli OCAMLC kernel/entries.ml OCAMLC kernel/modops.mli OCAMLC kernel/modops.ml OCAMLC kernel/type_errors.mli OCAMLC kernel/type_errors.ml OCAMLC kernel/inductive.mli OCAMLC kernel/inductive.ml OCAMLC kernel/typeops.mli OCAMLC kernel/typeops.ml File "kernel/typeops.ml", line 451, characters 5-59: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/indtypes.mli OCAMLC kernel/indtypes.ml OCAMLC kernel/cooking.mli OCAMLC kernel/cooking.ml OCAMLC kernel/term_typing.mli OCAMLC kernel/term_typing.ml File "kernel/term_typing.ml", line 34, characters 11-65: Warning X: this statement never returns (or has an unsound type.) OCAMLC kernel/subtyping.mli OCAMLC kernel/subtyping.ml OCAMLC kernel/mod_typing.mli OCAMLC kernel/mod_typing.ml OCAMLC kernel/safe_typing.mli OCAMLC kernel/safe_typing.ml OCAMLC -a -o kernel/kernel.cma OCAMLC library/nameops.mli OCAMLC library/nameops.ml OCAMLC library/libnames.mli OCAMLC library/libnames.ml OCAMLC library/libobject.mli OCAMLC library/libobject.ml OCAMLC library/summary.mli OCAMLC library/summary.ml OCAMLC library/nametab.mli OCAMLC -rectypes library/nametab.ml OCAMLC library/global.mli OCAMLC library/global.ml OCAMLC library/lib.mli OCAMLC library/lib.ml OCAMLC library/declaremods.mli OCAMLC library/declaremods.ml OCAMLC library/library.mli OCAMLC library/library.ml OCAMLC library/states.mli OCAMLC library/states.ml OCAMLC library/decl_kinds.ml OCAMLC library/dischargedhypsmap.mli OCAMLC library/dischargedhypsmap.ml OCAMLC library/goptions.mli OCAMLC library/goptions.ml OCAMLC -a -o library/library.cma OCAMLC pretyping/termops.mli OCAMLC pretyping/termops.ml OCAMLC pretyping/evd.mli OCAMLC pretyping/evd.ml OCAMLC pretyping/instantiate.mli OCAMLC pretyping/instantiate.ml OCAMLC pretyping/reductionops.mli OCAMLC pretyping/reductionops.ml OCAMLC pretyping/inductiveops.mli OCAMLC pretyping/inductiveops.ml OCAMLC pretyping/rawterm.mli OCAMLC pretyping/rawterm.ml OCAMLC pretyping/pattern.mli OCAMLC pretyping/pattern.ml OCAMLC pretyping/detyping.mli OCAMLC pretyping/detyping.ml OCAMLC pretyping/retyping.mli OCAMLC pretyping/retyping.ml OCAMLC pretyping/cbv.mli OCAMLC pretyping/cbv.ml OCAMLC pretyping/pretype_errors.mli OCAMLC pretyping/pretype_errors.ml OCAMLC pretyping/typing.mli OCAMLC pretyping/typing.ml OCAMLC pretyping/tacred.mli OCAMLC pretyping/tacred.ml OCAMLC pretyping/classops.mli OCAMLC pretyping/classops.ml OCAMLC pretyping/recordops.mli OCAMLC pretyping/recordops.ml OCAMLC pretyping/indrec.mli OCAMLC pretyping/indrec.ml OCAMLC pretyping/evarutil.mli OCAMLC pretyping/evarutil.ml OCAMLC pretyping/evarconv.mli OCAMLC pretyping/evarconv.ml OCAMLC pretyping/coercion.mli OCAMLC pretyping/coercion.ml OCAMLC pretyping/cases.mli OCAMLC pretyping/cases.ml OCAMLC pretyping/pretyping.mli OCAMLC pretyping/pretyping.ml OCAMLC pretyping/matching.mli OCAMLC pretyping/matching.ml OCAMLC -a -o pretyping/pretyping.cma OCAMLC parsing/lexer.mli OCAMLC4 parsing/lexer.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC interp/topconstr.mli OCAMLC interp/topconstr.ml OCAMLC interp/ppextend.mli OCAMLC interp/ppextend.ml OCAMLC interp/symbols.mli OCAMLC interp/symbols.ml OCAMLC interp/genarg.mli OCAMLC interp/genarg.ml OCAMLC interp/syntax_def.mli OCAMLC interp/syntax_def.ml OCAMLC interp/reserve.mli OCAMLC interp/reserve.ml OCAMLC library/impargs.mli OCAMLC library/impargs.ml OCAMLC parsing/coqast.mli OCAMLC interp/constrintern.mli OCAMLC interp/constrintern.ml OCAMLC interp/modintern.mli OCAMLC interp/modintern.ml OCAMLC interp/constrextern.mli OCAMLC interp/constrextern.ml OCAMLC interp/coqlib.mli OCAMLC interp/coqlib.ml OCAMLC library/declare.mli OCAMLC library/declare.ml OCAMLC -a -o interp/interp.cma OCAMLC parsing/coqast.ml OCAMLC parsing/ast.mli OCAMLC parsing/ast.ml OCAMLC parsing/termast.mli OCAMLC parsing/termast.ml OCAMLC parsing/extend.mli OCAMLC parsing/extend.ml OCAMLC parsing/esyntax.mli OCAMLC parsing/esyntax.ml OCAMLC -rectypes proofs/tacexpr.ml OCAMLC toplevel/vernacexpr.ml OCAMLC parsing/pcoq.mli OCAMLC4 parsing/pcoq.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC proofs/proof_type.mli OCAMLC parsing/pptactic.mli OCAMLC parsing/egrammar.mli OCAMLC parsing/egrammar.ml OCAMLC parsing/ppconstr.mli OCAMLC parsing/ppconstr.ml OCAMLC translate/ppconstrnew.mli OCAMLC translate/ppconstrnew.ml OCAMLC parsing/printer.mli OCAMLC parsing/printer.ml OCAMLC parsing/pptactic.ml OCAMLC translate/pptacticnew.mli OCAMLC translate/pptacticnew.ml OCAMLC parsing/printmod.mli OCAMLC parsing/printmod.ml OCAMLC parsing/prettyp.mli OCAMLC parsing/prettyp.ml OCAMLC parsing/search.mli OCAMLC parsing/search.ml OCAMLC -a -o parsing/parsing.cma OCAMLC proofs/proof_type.ml OCAMLC proofs/proof_trees.mli OCAMLC proofs/proof_trees.ml OCAMLC proofs/logic.mli OCAMLC proofs/logic.ml OCAMLC proofs/refiner.mli OCAMLC proofs/refiner.ml OCAMLC proofs/evar_refiner.mli OCAMLC proofs/evar_refiner.ml OCAMLC proofs/tacmach.mli OCAMLC proofs/tacmach.ml OCAMLC proofs/clenv.mli OCAMLC proofs/clenv.ml OCAMLC proofs/pfedit.mli OCAMLC proofs/pfedit.ml OCAMLC proofs/tactic_debug.mli OCAMLC proofs/tactic_debug.ml OCAMLC -a -o proofs/proofs.cma OCAMLC tactics/dn.mli OCAMLC tactics/dn.ml OCAMLC tactics/termdn.mli OCAMLC tactics/termdn.ml OCAMLC tactics/btermdn.mli OCAMLC tactics/btermdn.ml OCAMLC tactics/nbtermdn.mli OCAMLC tactics/nbtermdn.ml OCAMLC tactics/tacticals.mli OCAMLC tactics/tacticals.ml OCAMLC tactics/hipattern.mli OCAMLC tactics/hipattern.ml OCAMLC tactics/tactics.mli OCAMLC tactics/tactics.ml OCAMLC tactics/hiddentac.mli OCAMLC tactics/hiddentac.ml OCAMLC tactics/elim.mli OCAMLC tactics/elim.ml OCAMLC tactics/dhyp.mli OCAMLC tactics/dhyp.ml OCAMLC tactics/auto.mli OCAMLC tactics/auto.ml OCAMLC tactics/setoid_replace.mli OCAMLC tactics/setoid_replace.ml OCAMLC tactics/equality.mli OCAMLC tactics/equality.ml OCAMLC tactics/contradiction.mli OCAMLC tactics/contradiction.ml OCAMLC tactics/inv.mli OCAMLC tactics/inv.ml OCAMLC tactics/leminv.mli OCAMLC tactics/leminv.ml OCAMLC tactics/tacinterp.mli OCAMLC tactics/tacinterp.ml OCAMLC -a -o tactics/tactics.cma OCAMLC toplevel/himsg.mli OCAMLC toplevel/himsg.ml OCAMLC toplevel/cerrors.mli OCAMLC toplevel/cerrors.ml OCAMLC toplevel/class.mli OCAMLC toplevel/class.ml OCAMLC toplevel/metasyntax.mli OCAMLC toplevel/metasyntax.ml OCAMLC toplevel/command.mli OCAMLC toplevel/command.ml OCAMLC toplevel/record.mli OCAMLC toplevel/record.ml OCAMLC toplevel/recordobj.mli OCAMLC toplevel/recordobj.ml OCAMLC toplevel/discharge.mli OCAMLC toplevel/discharge.ml OCAMLC translate/ppvernacnew.mli OCAMLC translate/ppvernacnew.ml OCAMLC toplevel/vernacinterp.mli OCAMLC toplevel/vernacinterp.ml CAMLP4O toplevel/mltop.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC toplevel/mltop.mli OCAMLC toplevel/mltop.byteml OCAMLC toplevel/vernacentries.mli OCAMLC toplevel/vernacentries.ml OCAMLC toplevel/vernac.mli OCAMLC toplevel/vernac.ml OCAMLC toplevel/line_oriented_parser.mli OCAMLC toplevel/line_oriented_parser.ml OCAMLC toplevel/protectedtoplevel.mli OCAMLC toplevel/protectedtoplevel.ml OCAMLC toplevel/toplevel.mli OCAMLC toplevel/toplevel.ml OCAMLC toplevel/usage.mli OCAMLC toplevel/usage.ml OCAMLC toplevel/coqinit.mli OCAMLC toplevel/coqinit.ml OCAMLC toplevel/coqtop.mli OCAMLC toplevel/coqtop.ml OCAMLC -a -o toplevel/toplevel.cma OCAMLC4 parsing/g_prim.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_proofs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_basevernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_vernac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_tactic.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_ltac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_constr.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_cases.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_module.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC parsing/g_natsyntax.mli OCAMLC parsing/g_natsyntax.ml OCAMLC parsing/g_zsyntax.mli OCAMLC parsing/g_zsyntax.ml OCAMLC parsing/g_rsyntax.ml OCAMLC -a -o parsing/highparsing.cma OCAMLC4 parsing/g_primnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_constrnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_tacticnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_ltacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_vernacnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/g_proofsnew.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o parsing/highparsingnew.cma OCAMLC tactics/autorewrite.mli OCAMLC tactics/autorewrite.ml OCAMLC tactics/refine.mli OCAMLC tactics/refine.ml OCAMLC tactics/extraargs.mli OCAMLC parsing/q_util.mli OCAMLC4 parsing/q_util.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/q_coqast.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/argextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/tacextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 parsing/vernacextend.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a parsing/grammar.cma OCAMLC4 tactics/extraargs.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC tactics/extratactics.mli OCAMLC4 tactics/extratactics.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC tactics/eauto.mli OCAMLC4 tactics/eauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/tauto.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 tactics/eqdecide.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o tactics/hightactics.cma OCAMLC contrib/omega/omega.ml OCAMLC contrib/omega/coq_omega.ml OCAMLC4 contrib/omega/g_omega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/romega/omega2.ml OCAMLC contrib/romega/const_omega.ml OCAMLC contrib/romega/refl_omega.ml OCAMLC4 contrib/romega/g_romega.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/ring/quote.ml OCAMLC4 contrib/ring/g_quote.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/ring/ring.ml OCAMLC4 contrib/ring/g_ring.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/field/field.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/fourier/fourier.ml OCAMLC contrib/fourier/fourierR.ml OCAMLC4 contrib/fourier/g_fourier.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/extraction/miniml.mli OCAMLC contrib/extraction/table.mli OCAMLC contrib/extraction/table.ml OCAMLC contrib/extraction/mlutil.mli OCAMLC contrib/extraction/mlutil.ml OCAMLC contrib/extraction/modutil.mli OCAMLC contrib/extraction/modutil.ml OCAMLC contrib/extraction/ocaml.mli OCAMLC contrib/extraction/ocaml.ml OCAMLC contrib/extraction/haskell.mli OCAMLC contrib/extraction/haskell.ml OCAMLC contrib/extraction/scheme.mli OCAMLC contrib/extraction/scheme.ml OCAMLC contrib/extraction/extraction.mli OCAMLC contrib/extraction/extraction.ml OCAMLC contrib/extraction/common.mli OCAMLC contrib/extraction/common.ml OCAMLC contrib/extraction/extract_env.mli OCAMLC contrib/extraction/extract_env.ml OCAMLC4 contrib/extraction/g_extraction.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/jprover/opname.mli OCAMLC contrib/jprover/opname.ml OCAMLC contrib/jprover/jterm.mli OCAMLC contrib/jprover/jterm.ml OCAMLC contrib/jprover/jlogic.mli OCAMLC contrib/jprover/jlogic.ml OCAMLC contrib/jprover/jtunify.mli OCAMLC contrib/jprover/jtunify.ml OCAMLC contrib/jprover/jall.mli OCAMLC contrib/jprover/jall.ml OCAMLC4 contrib/jprover/jprover.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/unshare.mli OCAMLC contrib/xml/unshare.ml OCAMLC contrib/xml/xml.mli OCAMLC4 contrib/xml/xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/acic.ml OCAMLC contrib/xml/doubleTypeInference.mli OCAMLC contrib/xml/doubleTypeInference.ml OCAMLC contrib/xml/cic2acic.ml OCAMLC4 contrib/xml/acic2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/xml/proof2aproof.ml OCAMLC contrib/xml/xmlcommand.mli OCAMLC contrib/xml/xmlcommand.ml OCAMLC4 contrib/xml/proofTree2Xml.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC4 contrib/xml/xmlentries.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/cc/ccalgo.mli OCAMLC contrib/cc/ccalgo.ml OCAMLC contrib/cc/ccproof.mli OCAMLC contrib/cc/ccproof.ml OCAMLC4 contrib/cc/cctac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/funind/tacinvutils.mli OCAMLC contrib/funind/tacinvutils.ml OCAMLC4 contrib/funind/tacinv.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/first-order/formula.mli OCAMLC contrib/first-order/formula.ml OCAMLC contrib/first-order/unify.mli OCAMLC contrib/first-order/unify.ml OCAMLC contrib/first-order/sequent.mli OCAMLC contrib/first-order/sequent.ml OCAMLC contrib/first-order/rules.mli OCAMLC contrib/first-order/rules.ml OCAMLC contrib/first-order/instances.mli OCAMLC contrib/first-order/instances.ml OCAMLC contrib/first-order/ground.mli OCAMLC contrib/first-order/ground.ml OCAMLC4 contrib/first-order/g_ground.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -a -o contrib/contrib.cma COQMKTOP -o bin/coqtop.byte bin/coqtop.byte -boot -nois -compile theories/Init/Notations bin/coqtop.byte -boot -nois -compile theories/Init/Logic Defining 'IF' as keyword Defining 'exists2' as keyword bin/coqtop.byte -boot -nois -compile theories/Init/Datatypes bin/coqtop.byte -boot -nois -compile theories/Init/Peano bin/coqtop.byte -boot -nois -compile theories/Init/Specif bin/coqtop.byte -boot -nois -compile theories/Init/Logic_Type bin/coqtop.byte -boot -nois -compile theories/Init/Wf bin/coqtop.byte -boot -nois -compile theories/Init/Prelude bin/coqtop.byte -boot -batch -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq bin/coqtop.byte -boot -compile theories/Logic/Hurkens bin/coqtop.byte -boot -compile theories/Logic/ProofIrrelevance bin/coqtop.byte -boot -compile theories/Logic/Classical_Prop bin/coqtop.byte -boot -compile theories/Logic/Classical_Pred_Type bin/coqtop.byte -boot -compile theories/Logic/Classical bin/coqtop.byte -boot -compile theories/Logic/Classical_Type bin/coqtop.byte -boot -compile theories/Logic/Classical_Pred_Set bin/coqtop.byte -boot -compile theories/Logic/Eqdep bin/coqtop.byte -boot -compile theories/Logic/ClassicalFacts bin/coqtop.byte -boot -compile theories/Logic/ChoiceFacts bin/coqtop.byte -boot -compile theories/Logic/Berardi bin/coqtop.byte -boot -compile theories/Logic/Eqdep_dec bin/coqtop.byte -boot -compile theories/Logic/Decidable bin/coqtop.byte -boot -compile theories/Logic/JMeq bin/coqtop.byte -boot -compile theories/Logic/ClassicalDescription bin/coqtop.byte -boot -compile theories/Logic/RelationalChoice bin/coqtop.byte -boot -compile theories/Logic/ClassicalChoice bin/coqtop.byte -boot -compile theories/Bool/Bool bin/coqtop.byte -boot -compile theories/Logic/Diaconescu bin/coqtop.byte -boot -compile theories/Arith/Le bin/coqtop.byte -boot -compile theories/Arith/Lt bin/coqtop.byte -boot -compile theories/Arith/Plus bin/coqtop.byte -boot -compile theories/Arith/Gt bin/coqtop.byte -boot -compile theories/Arith/Minus bin/coqtop.byte -boot -compile theories/Arith/Mult bin/coqtop.byte -boot -compile theories/Arith/Between bin/coqtop.byte -boot -compile theories/Arith/Peano_dec bin/coqtop.byte -boot -compile theories/Arith/Compare_dec bin/coqtop.byte -boot -compile theories/Arith/Factorial bin/coqtop.byte -boot -compile theories/Arith/Arith bin/coqtop.byte -boot -compile theories/Arith/Wf_nat bin/coqtop.byte -boot -compile theories/Arith/Min bin/coqtop.byte -boot -compile theories/Arith/Compare bin/coqtop.byte -boot -compile theories/Arith/Even bin/coqtop.byte -boot -compile theories/Arith/Div2 bin/coqtop.byte -boot -compile theories/Arith/EqNat bin/coqtop.byte -boot -compile theories/Arith/Euclid bin/coqtop.byte -boot -compile theories/Arith/Max bin/coqtop.byte -boot -compile theories/Bool/Sumbool bin/coqtop.byte -boot -compile theories/Arith/Bool_nat bin/coqtop.byte -boot -compile theories/Bool/IfProp bin/coqtop.byte -boot -compile theories/Bool/Zerob bin/coqtop.byte -boot -compile theories/Bool/DecBool bin/coqtop.byte -boot -compile theories/Bool/BoolEq bin/coqtop.byte -boot -compile theories/Bool/Bvector bin/coqtop.byte -boot -compile theories/NArith/BinPos bin/coqtop.byte -boot -compile theories/NArith/Pnat bin/coqtop.byte -boot -compile theories/NArith/BinNat bin/coqtop.byte -boot -compile theories/NArith/NArith bin/coqtop.byte -boot -compile theories/ZArith/BinInt bin/coqtop.byte -boot -compile theories/ZArith/Zcompare bin/coqtop.byte -boot -compile theories/ZArith/Zorder bin/coqtop.byte -boot -compile theories/ZArith/Znat bin/coqtop.byte -boot -compile theories/ZArith/Zmisc bin/coqtop.byte -boot -compile theories/ZArith/Wf_Z bin/coqtop.byte -boot -compile theories/ZArith/Zeven bin/coqtop.byte -boot -compile theories/ZArith/Zmin bin/coqtop.byte -boot -compile theories/ZArith/ZArith_dec bin/coqtop.byte -boot -compile theories/ZArith/Zabs bin/coqtop.byte -boot -compile theories/ZArith/auxiliary bin/coqtop.byte -boot -compile theories/ZArith/Zbool bin/coqtop.byte -boot -compile theories/ZArith/Zhints bin/coqtop.byte -boot -compile theories/ZArith/ZArith_base bin/coqtop.byte -boot -compile contrib/ring/Ring_theory bin/coqtop.byte -boot -compile contrib/ring/Quote bin/coqtop.byte -boot -compile contrib/ring/Ring_normalize bin/coqtop.byte -boot -compile contrib/ring/Ring_abstract bin/coqtop.byte -boot -compile contrib/ring/Ring bin/coqtop.byte -boot -compile contrib/ring/ArithRing bin/coqtop.byte -boot -compile contrib/ring/ZArithRing bin/coqtop.byte -boot -compile contrib/omega/OmegaLemmas bin/coqtop.byte -boot -compile contrib/omega/Omega bin/coqtop.byte -boot -compile theories/Lists/List bin/coqtop.byte -boot -compile theories/ZArith/Zcomplements bin/coqtop.byte -boot -compile theories/ZArith/Zsqrt bin/coqtop.byte -boot -compile theories/ZArith/Zpower bin/coqtop.byte -boot -compile theories/ZArith/Zdiv Defining 'mod' as keyword bin/coqtop.byte -boot -compile theories/ZArith/Zlogarithm bin/coqtop.byte -boot -compile theories/ZArith/ZArith bin/coqtop.byte -boot -compile theories/ZArith/Zwf bin/coqtop.byte -boot -compile theories/ZArith/Zbinary bin/coqtop.byte -boot -compile theories/ZArith/Znumtheory bin/coqtop.byte -boot -compile theories/Lists/MonoList bin/coqtop.byte -boot -compile theories/Lists/ListSet bin/coqtop.byte -boot -compile theories/Lists/Streams bin/coqtop.byte -boot -compile theories/Lists/TheoryList bin/coqtop.byte -boot -compile theories/Sets/Ensembles bin/coqtop.byte -boot -compile theories/Sets/Constructive_sets bin/coqtop.byte -boot -compile theories/Sets/Classical_sets bin/coqtop.byte -boot -compile theories/Sets/Permut bin/coqtop.byte -boot -compile theories/Sets/Relations_1 bin/coqtop.byte -boot -compile theories/Sets/Relations_1_facts bin/coqtop.byte -boot -compile theories/Sets/Partial_Order bin/coqtop.byte -boot -compile theories/Sets/Cpo bin/coqtop.byte -boot -compile theories/Sets/Powerset bin/coqtop.byte -boot -compile theories/Sets/Powerset_facts bin/coqtop.byte -boot -compile theories/Sets/Powerset_Classical_facts bin/coqtop.byte -boot -compile theories/Sets/Finite_sets bin/coqtop.byte -boot -compile theories/Sets/Finite_sets_facts bin/coqtop.byte -boot -compile theories/Sets/Image bin/coqtop.byte -boot -compile theories/Sets/Relations_2 bin/coqtop.byte -boot -compile theories/Sets/Infinite_sets bin/coqtop.byte -boot -compile theories/Sets/Relations_2_facts bin/coqtop.byte -boot -compile theories/Sets/Integers bin/coqtop.byte -boot -compile theories/Sets/Relations_3 bin/coqtop.byte -boot -compile theories/Sets/Multiset bin/coqtop.byte -boot -compile theories/Sets/Relations_3_facts bin/coqtop.byte -boot -compile theories/Sets/Uniset bin/coqtop.byte -boot -compile theories/IntMap/Addr bin/coqtop.byte -boot -compile theories/IntMap/Adist bin/coqtop.byte -boot -compile theories/IntMap/Addec bin/coqtop.byte -boot -compile theories/IntMap/Map bin/coqtop.byte -boot -compile theories/IntMap/Fset bin/coqtop.byte -boot -compile theories/IntMap/Adalloc bin/coqtop.byte -boot -compile theories/IntMap/Mapaxioms bin/coqtop.byte -boot -compile theories/IntMap/Mapiter bin/coqtop.byte -boot -compile theories/IntMap/Lsort bin/coqtop.byte -boot -compile theories/IntMap/Mapsubset bin/coqtop.byte -boot -compile theories/IntMap/Mapcard bin/coqtop.byte -boot -compile theories/IntMap/Mapcanon bin/coqtop.byte -boot -compile theories/IntMap/Mapc bin/coqtop.byte -boot -compile theories/IntMap/Mapfold bin/coqtop.byte -boot -compile theories/IntMap/Maplists bin/coqtop.byte -boot -compile theories/IntMap/Allmaps bin/coqtop.byte -boot -compile theories/Relations/Rstar bin/coqtop.byte -boot -compile theories/Relations/Newman bin/coqtop.byte -boot -compile theories/Relations/Relation_Definitions bin/coqtop.byte -boot -compile theories/Relations/Relation_Operators bin/coqtop.byte -boot -compile theories/Relations/Operators_Properties bin/coqtop.byte -boot -compile theories/Relations/Relations bin/coqtop.byte -boot -compile theories/Wellfounded/Disjoint_Union bin/coqtop.byte -boot -compile theories/Wellfounded/Inclusion bin/coqtop.byte -boot -compile theories/Wellfounded/Inverse_Image bin/coqtop.byte -boot -compile theories/Wellfounded/Transitive_Closure bin/coqtop.byte -boot -compile theories/Wellfounded/Lexicographic_Exponentiation bin/coqtop.byte -boot -compile theories/Wellfounded/Union bin/coqtop.byte -boot -compile theories/Wellfounded/Lexicographic_Product bin/coqtop.byte -boot -compile theories/Wellfounded/Well_Ordering bin/coqtop.byte -boot -compile theories/Wellfounded/Wellfounded bin/coqtop.byte -boot -compile theories/Reals/Rdefinitions bin/coqtop.byte -boot -compile theories/Reals/Raxioms bin/coqtop.byte -boot -compile contrib/field/Field_Compl bin/coqtop.byte -boot -compile contrib/field/Field_Theory bin/coqtop.byte -boot -compile contrib/field/Field_Tactic bin/coqtop.byte -boot -compile contrib/field/Field bin/coqtop.byte -boot -compile theories/Reals/RIneq bin/coqtop.byte -boot -compile theories/Reals/DiscrR bin/coqtop.byte -boot -compile theories/Reals/Rbase bin/coqtop.byte -boot -compile theories/Reals/R_Ifp bin/coqtop.byte -boot -compile contrib/fourier/Fourier_util bin/coqtop.byte -boot -compile contrib/fourier/Fourier bin/coqtop.byte -boot -compile theories/Reals/Rbasic_fun bin/coqtop.byte -boot -compile theories/Reals/R_sqr bin/coqtop.byte -boot -compile theories/Reals/SplitAbsolu bin/coqtop.byte -boot -compile theories/Reals/SplitRmult bin/coqtop.byte -boot -compile theories/Reals/ArithProp bin/coqtop.byte -boot -compile theories/Reals/Rfunctions bin/coqtop.byte -boot -compile theories/Reals/Rseries bin/coqtop.byte -boot -compile theories/Reals/SeqProp bin/coqtop.byte -boot -compile theories/Reals/Rcomplete bin/coqtop.byte -boot -compile theories/Reals/PartSum bin/coqtop.byte -boot -compile theories/Reals/AltSeries bin/coqtop.byte -boot -compile theories/Reals/Binomial bin/coqtop.byte -boot -compile theories/Reals/Rsigma bin/coqtop.byte -boot -compile theories/Reals/Rprod bin/coqtop.byte -boot -compile theories/Reals/Cauchy_prod bin/coqtop.byte -boot -compile theories/Reals/Alembert bin/coqtop.byte -boot -compile theories/Reals/SeqSeries bin/coqtop.byte -boot -compile theories/Reals/Rtrigo_fun bin/coqtop.byte -boot -compile theories/Reals/Rtrigo_def bin/coqtop.byte -boot -compile theories/Reals/Rtrigo_alt bin/coqtop.byte -boot -compile theories/Reals/Cos_rel bin/coqtop.byte -boot -compile theories/Reals/Cos_plus bin/coqtop.byte -boot -compile theories/Reals/Rtrigo bin/coqtop.byte -boot -compile theories/Reals/Rlimit bin/coqtop.byte -boot -compile theories/Reals/Rderiv bin/coqtop.byte -boot -compile theories/Reals/RList bin/coqtop.byte -boot -compile theories/Reals/Ranalysis1 Defining 'o' as keyword bin/coqtop.byte -boot -compile theories/Reals/Ranalysis2 bin/coqtop.byte -boot -compile theories/Reals/Ranalysis3 bin/coqtop.byte -boot -compile theories/Reals/Rtopology bin/coqtop.byte -boot -compile theories/Reals/MVT bin/coqtop.byte -boot -compile theories/Reals/PSeries_reg bin/coqtop.byte -boot -compile theories/Reals/Exp_prop bin/coqtop.byte -boot -compile theories/Reals/Rtrigo_reg bin/coqtop.byte -boot -compile theories/Reals/Rsqrt_def bin/coqtop.byte -boot -compile theories/Reals/R_sqrt bin/coqtop.byte -boot -compile theories/Reals/Rtrigo_calc bin/coqtop.byte -boot -compile theories/Reals/Rgeom bin/coqtop.byte -boot -compile theories/Reals/Sqrt_reg bin/coqtop.byte -boot -compile theories/Reals/Ranalysis4 bin/coqtop.byte -boot -compile theories/Reals/Rpower bin/coqtop.byte -boot -compile theories/Reals/Ranalysis bin/coqtop.byte -boot -compile theories/Reals/NewtonInt bin/coqtop.byte -boot -compile theories/Reals/RiemannInt_SF bin/coqtop.byte -boot -compile theories/Reals/RiemannInt bin/coqtop.byte -boot -compile theories/Reals/Integration bin/coqtop.byte -boot -compile theories/Reals/Reals bin/coqtop.byte -boot -compile theories/Setoids/Setoid bin/coqtop.byte -boot -compile theories/Sorting/Permutation bin/coqtop.byte -boot -compile theories/Sorting/Sorting bin/coqtop.byte -boot -compile theories/Sorting/Heap bin/coqtop.byte -boot -compile contrib/romega/ReflOmegaCore Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable bin/coqtop.byte -boot -compile contrib/romega/ROmega bin/coqtop.byte -boot -compile contrib/ring/NArithRing bin/coqtop.byte -boot -compile contrib/ring/Setoid_ring_theory bin/coqtop.byte -boot -compile contrib/ring/Setoid_ring_normalize bin/coqtop.byte -boot -compile contrib/ring/Setoid_ring bin/coqtop.byte -boot -compile contrib/cc/CCSolve OCAMLLEX tools/coqdep_lexer.mll 187 states, 5170 transitions, table size 21802 bytes OCAMLC tools/coqdep_lexer.ml OCAMLC tools/coqdep.ml OCAMLC -o bin/coqdep OCAMLC4 tools/coq_makefile.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -o bin/coq_makefile OCAMLLEX tools/gallina_lexer.mll 151 states, 498 transitions, table size 2898 bytes OCAMLC tools/gallina_lexer.ml OCAMLC tools/gallina.ml File "tools/gallina.ml", line 25, characters 20-44: Warning X: this statement never returns (or has an unsound type.) File "tools/gallina.ml", line 38, characters 20-44: Warning X: this statement never returns (or has an unsound type.) OCAMLC -o bin/gallina OCAMLC4 tools/coq-tex.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC -o bin/coq-tex OCAMLLEX tools/coqwc.mll 148 states, 742 transitions, table size 3856 bytes OCAMLC tools/coqwc.ml OCAMLC -o bin/coqwc OCAMLC tools/coqdoc/alpha.mli OCAMLC tools/coqdoc/alpha.ml OCAMLC tools/coqdoc/index.mli OCAMLLEX tools/coqdoc/index.mll 166 states, 4253 transitions, table size 18008 bytes OCAMLC tools/coqdoc/index.ml OCAMLC tools/coqdoc/output.mli OCAMLC tools/coqdoc/output.ml OCAMLC tools/coqdoc/pretty.mli OCAMLLEX tools/coqdoc/pretty.mll 477 states, 19341 transitions, table size 80226 bytes OCAMLC tools/coqdoc/pretty.ml OCAMLC tools/coqdoc/main.ml OCAMLC -o bin/coqdoc OCAMLC dev/top_printers.ml OCAMLC scripts/coqc.ml OCAMLC -o bin/coqc cd bin; ln -sf coqtop.byte coqtop bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Notations bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Logic bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Datatypes bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Peano bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Specif bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Logic_Type bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Wf bin/coqtop.byte -boot -translate -strict-implicit -nois -compile theories7/Init/Prelude bin/coqtop.byte -v7 -boot -batch -silent -nois -I syntax -load-vernac-source syntax/MakeBare.v -outputstate states7/barestate.coq bin/coqtop.byte -boot -v7 -batch -silent -is states7/barestate.coq -load-vernac-source states7/MakeInitial.v -outputstate states7/initial.coq bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Hurkens bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/ProofIrrelevance bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Classical_Prop bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Classical_Pred_Type bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Classical bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Classical_Type bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Classical_Pred_Set bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Eqdep bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/ClassicalFacts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/ChoiceFacts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Berardi bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Eqdep_dec Warning: Capture check in multiple binders not done Warning: Capture check in multiple binders not done bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Decidable bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/JMeq bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/ClassicalDescription bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/RelationalChoice bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/ClassicalChoice bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/Bool bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Logic/Diaconescu bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Le bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Lt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Plus bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Gt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Minus bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Mult bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Between bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Peano_dec bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Compare_dec bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Factorial bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Arith bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Wf_nat bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Min bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Compare bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Even bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Div2 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/EqNat bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Euclid bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Max bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/Sumbool bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Arith/Bool_nat bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/IfProp bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/Zerob bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/DecBool bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/BoolEq bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Bool/Bvector bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/NArith/BinPos Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition [fact:=(Prec positive xH [p,r:positive](times (add_un p) r))] [seven:=(xI (xI xH))] [five_thousand_forty:= (xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH))))))))))))] ((refl_equal positive (fact seven))::(fact seven)=five_thousand_forty) : (Prec positive xH [p,r:positive](times (add_un p) r) (xI (xI xH))) =(xO (xO (xO (xO (xI (xI (xO (xI (xI (xI (xO (xO xH)))))))))))) Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition Translator warning: Unable to detect if H denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/NArith/Pnat bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/NArith/BinNat Translator warning: Unable to detect if H denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/NArith/NArith bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/BinInt Translator warning: Unable to detect if H denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zsyntax bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zcompare bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zorder Warning: Forgetting obsolete module Zsyntax Translator warning: Unable to detect if H denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Znat bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zeven bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/ZArith_dec bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zbool bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zabs bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zmin bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zmisc bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Wf_Z bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/fast_integer bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/zarith_aux bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/auxiliary bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zhints bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/ZArith_base bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Ring_theory bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Quote bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Ring_normalize bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Ring_abstract Translator warning: Unable to detect if H0 denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Ring bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/ArithRing bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/ZArithRing bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/omega/OmegaLemmas bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/omega/Omega bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/PolyList bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zcomplements bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zsqrt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zpower bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zdiv bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zlogarithm bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/ZArith bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zwf bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Zbinary bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/ZArith/Znumtheory bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/MonoList bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/ListSet bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/Streams bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/TheoryList bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/List bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Ensembles bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Constructive_sets bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Classical_sets bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Permut bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_1 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_1_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Partial_Order bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Cpo bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Powerset bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Powerset_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Powerset_Classical_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Finite_sets bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Finite_sets_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Image bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_2 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Infinite_sets bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_2_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Integers bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_3 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Multiset bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Relations_3_facts bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sets/Uniset bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Addr bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Adist bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Addec bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Map bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Fset bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Adalloc bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapaxioms bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapiter bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Lsort bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapsubset bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapcard bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapcanon bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapc bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Mapfold bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Maplists bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/IntMap/Allmaps bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Rstar bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Newman bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Relation_Definitions bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Lists/PolyListSyntax bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Relation_Operators bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Operators_Properties bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Relations/Relations bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Disjoint_Union bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Inclusion bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Inverse_Image bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Transitive_Closure bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Lexicographic_Exponentiation bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Union bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Lexicographic_Product bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Well_Ordering bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Wellfounded/Wellfounded bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rdefinitions bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rsyntax bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Raxioms bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/field/Field_Compl bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/field/Field_Theory bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/field/Field_Tactic bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/field/Field bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/RIneq bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/DiscrR bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rbase bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/R_Ifp bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/fourier/Fourier_util bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/fourier/Fourier bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rbasic_fun bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/R_sqr bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/SplitAbsolu bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/SplitRmult bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/ArithProp bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rfunctions bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rseries bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/SeqProp bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rcomplete bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/PartSum Translator warning: Unable to detect if r denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/AltSeries bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Binomial bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rsigma bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rprod bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Cauchy_prod bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Alembert bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/SeqSeries bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_fun bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_def bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_alt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Cos_rel bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Cos_plus bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rlimit bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rderiv bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/RList bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis1 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis2 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis3 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtopology bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/MVT bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/PSeries_reg bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Exp_prop bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_reg bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rsqrt_def bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/R_sqrt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rtrigo_calc bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rgeom bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Sqrt_reg bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis4 bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Rpower bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Ranalysis bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/NewtonInt bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/RiemannInt_SF bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/RiemannInt Translator warning: Unable to detect if u0 denotes a local definition Translator warning: Unable to detect if H1 denotes a local definition Translator warning: Unable to detect if H3 denotes a local definition Translator warning: Unable to detect if H8 denotes a local definition bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Integration bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Reals/Reals bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Setoids/Setoid bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sorting/Permutation bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sorting/Sorting bin/coqtop.byte -boot -translate -strict-implicit -compile theories7/Sorting/Heap bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/romega/ReflOmegaCore Warning: unable to ensure the correctness of the translation of an if-then-else Warning: unable to ensure the correctness of the translation of an if-then-else Warning: unable to ensure the correctness of the translation of an if-then-else Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable Warning: pattern step is understood as a pattern variable bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/romega/ROmega bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/NArithRing bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_theory bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring_normalize bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/ring/Setoid_ring bin/coqtop.byte -boot -translate -strict-implicit -compile contrib7/cc/CCSolve bin/coqtop.byte -boot -compile ide/utf8 OCAMLC ide/utils/okey.mli OCAMLC ide/utils/okey.ml OCAMLC ide/utils/uoptions.mli OCAMLC ide/utils/uoptions.ml OCAMLC ide/utils/configwin_keys.ml OCAMLC ide/utils/configwin_types.ml OCAMLC ide/utils/configwin_messages.ml OCAMLC ide/utils/configwin_ihm.ml OCAMLC ide/utils/configwin.mli OCAMLC ide/utils/configwin.ml OCAMLC ide/utils/editable_cells.ml File "ide/utils/editable_cells.ml", line 88, characters 10-36: Warning S: this expression should have type unit. OCAMLYACC ide/config_parser.mly OCAMLC ide/config_parser.mli OCAMLYACC ide/config_parser.mly OCAMLC ide/config_parser.ml OCAMLLEX ide/config_lexer.mll 13 states, 332 transitions, table size 1406 bytes OCAMLC ide/config_lexer.ml OCAMLLEX ide/utf8_convert.mll 15 states, 827 transitions, table size 3398 bytes OCAMLC ide/utf8_convert.ml OCAMLC ide/preferences.mli OCAMLC ide/preferences.ml OCAMLC ide/ideutils.mli OCAMLC ide/ideutils.ml OCAMLC ide/coq.mli OCAMLC ide/blaster_window.ml OCAMLC ide/undo.mli Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC ide/undo.ml OCAMLLEX ide/find_phrase.mll 15 states, 265 transitions, table size 1150 bytes OCAMLC ide/find_phrase.ml OCAMLLEX ide/highlight.mll 198 states, 1082 transitions, table size 5516 bytes OCAMLC ide/highlight.ml OCAMLC ide/coq.ml OCAMLC ide/coq_commands.ml OCAMLC ide/coq_tactics.mli OCAMLC ide/coq_tactics.ml OCAMLC ide/command_windows.mli OCAMLC ide/command_windows.ml OCAMLC ide/coqide.mli OCAMLC ide/coqide.ml OCAMLC -a -o ide/ide.cma COQMKTOP -o bin/coqide.byte cd bin; ln -sf coqide.byte coqide OCAMLC contrib/interface/ascent.mli OCAMLC contrib/interface/vtp.mli OCAMLC contrib/interface/vtp.ml OCAMLC contrib/interface/xlate.mli OCAMLC contrib/interface/xlate.ml OCAMLC contrib/interface/paths.mli OCAMLC contrib/interface/paths.ml OCAMLC contrib/interface/ctast.ml OCAMLC contrib/interface/translate.mli OCAMLC contrib/interface/translate.ml OCAMLC contrib/interface/pbp.mli OCAMLC contrib/interface/pbp.ml OCAMLC contrib/interface/dad.mli OCAMLC contrib/interface/dad.ml OCAMLC contrib/interface/history.mli OCAMLC contrib/interface/history.ml OCAMLC contrib/interface/name_to_ast.mli OCAMLC contrib/interface/name_to_ast.ml OCAMLC contrib/interface/debug_tac.mli OCAMLC4 contrib/interface/debug_tac.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/interface/showproof_ct.ml OCAMLC contrib/interface/showproof.mli OCAMLC contrib/interface/showproof.ml OCAMLC contrib/interface/blast.mli OCAMLC contrib/interface/blast.ml OCAMLC4 contrib/interface/centaur.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. File "contrib/interface/centaur.ml4", line 364, characters 4-180: Warning X: this statement never returns (or has an unsound type.) COQMKTOP -o bin/coq-interface OCAMLC contrib/interface/line_parser.mli OCAMLC4 contrib/interface/line_parser.ml4 Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead. OCAMLC contrib/interface/parse.ml OCAMLC -o bin/parser cd test-suite; \ env COQBIN=../bin COQLIB=.. ./check -byte | tee check.log [Output tests are off] Success tests success/Case1.v...Ok success/Case10.v...Ok success/Case11.v...Ok success/Case12.v...Ok success/Case13.v...Ok success/Case14.v...Ok success/Case15.v...Ok success/Case16.v...Ok success/Case17.v...Ok success/Case2.v...Ok success/Case5.v...Ok success/Case6.v...Ok success/Case7.v...Ok success/Case9.v...Ok success/CaseAlias.v...Ok success/Cases.v...Ok success/CasesDep.v...Ok success/Check.v...Ok success/Conjecture.v...Ok success/DHyp.v...Ok success/Decompose.v...Ok success/Destruct.v...Ok success/DiscrR.v...Ok success/Discriminate.v...Ok success/Field.v...Ok success/Fourier.v...Ok success/Funind.v...Ok success/Generalize.v...Ok success/Hints.v...Ok success/Inductive.v...Ok success/Injection.v...Ok success/Inversion.v...Ok success/LetIn.v...Ok success/MatchFail.v...Ok success/Mod_ltac.v...Ok success/Mod_params.v...Ok success/Mod_strengthen.v...Ok success/NatRing.v...Ok success/Omega.v...Ok success/Print.v...Ok success/Projection.v...Ok success/Record.v...Ok success/Reg.v...Ok success/Remark.v...Ok success/Rename.v...Ok success/Require.v...Ok success/Scopes.v...Ok success/Simplify_eq.v...Ok success/Tauto.v...Ok success/TestRefine.v...Ok success/Try.v...Ok success/cc.v...Ok success/coercions.v...Ok success/coqbugs0181.v...Ok success/eauto.v...Ok success/eqdecide.v...Ok success/evars.v...Ok success/fix.v...Ok success/if.v...Ok success/implicit.v...Ok success/import_lib.v...Ok success/import_mod.v...Ok success/inds_type_sec.v...Ok success/induct.v...Ok success/ltac.v...Ok success/mutual_ind.v...Ok success/options.v...Ok success/refine.v...Ok success/setoid_test.v...Ok success/unfold.v...Ok success/univers.v...Ok success/Abstract.v8...Ok success/PPFix.v8...Ok success/RecTutorial.v8...Ok Failure tests failure/Case1.v...Ok failure/Case10.v...Ok failure/Case11.v...Ok failure/Case12.v...Ok failure/Case13.v...Ok failure/Case14.v...Ok failure/Case15.v...Ok failure/Case16.v...Ok failure/Case2.v...Ok failure/Case3.v...Ok failure/Case4.v...Ok failure/Case5.v...Ok failure/Case6.v...Ok failure/Case7.v...Ok failure/Case8.v...Ok failure/Case9.v...Ok failure/ClearBody.v...Ok failure/Tauto.v...Ok failure/cases.v...Ok failure/check.v...Ok failure/clash_cons.v...Ok failure/clashes.v...Ok failure/coqbugs0266.v...Ok failure/fixpoint1.v...Ok failure/illtype1.v...Ok failure/ltac1.v...Ok failure/ltac2.v...Ok failure/ltac3.v...Ok failure/ltac4.v...Ok failure/params_ind.v...Ok failure/positivity.v...Ok failure/redef.v...Ok failure/search.v...Ok failure/universes-buraliforti.v...Ok failure/universes-sections1.v...Ok failure/universes-sections2.v...Ok failure/universes.v...Ok failure/universes2.v...Ok Parser tests 112 tests passed over 112, i.e. 100 % if grep -F 'Error!' test-suite/check.log ; then false; fi make[1]: Leaving directory `/build/buildd/coq-8.0pl3' NATIVE CODE COMPILATION FAILED Coq was built in bytecode instead touch build-stamp /usr/bin/fakeroot debian/rules binary-arch dh_testdir dh_testroot dh_clean -k dh_installdirs if [ -e opt-stamp ]; then \ /usr/bin/make COQINSTALLPREFIX=/build/buildd/coq-8.0pl3/debian/tmp install; \ else \ /usr/bin/make BEST=byte HASCOQIDE=byte COQINSTALLPREFIX=/build/buildd/coq-8.0pl3/debian/tmp install; \ fi make[1]: Entering directory `/build/buildd/coq-8.0pl3' mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cp bin/coqmktop bin/coqc bin/coqtop.byte '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cd '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin'; ln -sf coqtop.byte coqtop mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cp bin/coqdep bin/coq_makefile bin/gallina bin/coq-tex bin/coqwc bin/coqdoc '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq' for f in theories7/Init/Notations.vo theories7/Init/Datatypes.vo theories7/Init/Peano.vo theories7/Init/Logic.vo theories7/Init/Specif.vo theories7/Init/Logic_Type.vo theories7/Init/Wf.vo theories7/Init/Prelude.vo theories7/Logic/Hurkens.vo theories7/Logic/ProofIrrelevance.vo theories7/Logic/Classical.vo theories7/Logic/Classical_Type.vo theories7/Logic/Classical_Pred_Set.vo theories7/Logic/Eqdep.vo theories7/Logic/Classical_Pred_Type.vo theories7/Logic/Classical_Prop.vo theories7/Logic/ClassicalFacts.vo theories7/Logic/ChoiceFacts.vo theories7/Logic/Berardi.vo theories7/Logic/Eqdep_dec.vo theories7/Logic/Decidable.vo theories7/Logic/JMeq.vo theories7/Logic/ClassicalDescription.vo theories7/Logic/ClassicalChoice.vo theories7/Logic/RelationalChoice.vo theories7/Logic/Diaconescu.vo theories7/Arith/Arith.vo theories7/Arith/Gt.vo theories7/Arith/Between.vo theories7/Arith/Le.vo theories7/Arith/Compare.vo theories7/Arith/Lt.vo theories7/Arith/Compare_dec.vo theories7/Arith/Min.vo theories7/Arith/Div2.vo theories7/Arith/Minus.vo theories7/Arith/Mult.vo theories7/Arith/Even.vo theories7/Arith/EqNat.vo theories7/Arith/Peano_dec.vo theories7/Arith/Euclid.vo theories7/Arith/Plus.vo theories7/Arith/Wf_nat.vo theories7/Arith/Max.vo theories7/Arith/Bool_nat.vo theories7/Arith/Factorial.vo theories7/Bool/Bool.vo theories7/Bool/IfProp.vo theories7/Bool/Zerob.vo theories7/Bool/DecBool.vo theories7/Bool/Sumbool.vo theories7/Bool/BoolEq.vo theories7/Bool/Bvector.vo theories7/NArith/BinPos.vo theories7/NArith/Pnat.vo theories7/NArith/BinNat.vo theories7/NArith/NArith.vo theories7/ZArith/BinInt.vo theories7/ZArith/Wf_Z.vo theories7/ZArith/ZArith.vo theories7/ZArith/ZArith_dec.vo theories7/ZArith/auxiliary.vo theories7/ZArith/Zmisc.vo theories7/ZArith/Zcompare.vo theories7/ZArith/Znat.vo theories7/ZArith/Zorder.vo theories7/ZArith/Zabs.vo theories7/ZArith/Zmin.vo theories7/ZArith/Zeven.vo theories7/ZArith/Zhints.vo theories7/ZArith/Zlogarithm.vo theories7/ZArith/Zpower.vo theories7/ZArith/Zcomplements.vo theories7/ZArith/Zdiv.vo theories7/ZArith/Zsqrt.vo theories7/ZArith/Zwf.vo theories7/ZArith/ZArith_base.vo theories7/ZArith/Zbool.vo theories7/ZArith/Zbinary.vo theories7/ZArith/Znumtheory.vo theories7/Lists/MonoList.vo theories7/Lists/ListSet.vo theories7/Lists/Streams.vo theories7/Lists/TheoryList.vo theories7/Lists/List.vo theories7/Sets/Classical_sets.vo theories7/Sets/Permut.vo theories7/Sets/Constructive_sets.vo theories7/Sets/Powerset.vo theories7/Sets/Cpo.vo theories7/Sets/Powerset_Classical_facts.vo theories7/Sets/Ensembles.vo theories7/Sets/Powerset_facts.vo theories7/Sets/Finite_sets.vo theories7/Sets/Relations_1.vo theories7/Sets/Finite_sets_facts.vo theories7/Sets/Relations_1_facts.vo theories7/Sets/Image.vo theories7/Sets/Relations_2.vo theories7/Sets/Infinite_sets.vo theories7/Sets/Relations_2_facts.vo theories7/Sets/Integers.vo theories7/Sets/Relations_3.vo theories7/Sets/Multiset.vo theories7/Sets/Relations_3_facts.vo theories7/Sets/Partial_Order.vo theories7/Sets/Uniset.vo theories7/IntMap/Adalloc.vo theories7/IntMap/Mapcanon.vo theories7/IntMap/Addec.vo theories7/IntMap/Mapcard.vo theories7/IntMap/Addr.vo theories7/IntMap/Mapc.vo theories7/IntMap/Adist.vo theories7/IntMap/Mapfold.vo theories7/IntMap/Allmaps.vo theories7/IntMap/Mapiter.vo theories7/IntMap/Fset.vo theories7/IntMap/Maplists.vo theories7/IntMap/Lsort.vo theories7/IntMap/Mapsubset.vo theories7/IntMap/Mapaxioms.vo theories7/IntMap/Map.vo theories7/Relations/Newman.vo theories7/Relations/Operators_Properties.vo theories7/Relations/Relation_Definitions.vo theories7/Relations/Relation_Operators.vo theories7/Relations/Relations.vo theories7/Relations/Rstar.vo theories7/Wellfounded/Disjoint_Union.vo theories7/Wellfounded/Inclusion.vo theories7/Wellfounded/Inverse_Image.vo theories7/Wellfounded/Lexicographic_Exponentiation.vo theories7/Wellfounded/Transitive_Closure.vo theories7/Wellfounded/Union.vo theories7/Wellfounded/Wellfounded.vo theories7/Wellfounded/Well_Ordering.vo theories7/Wellfounded/Lexicographic_Product.vo theories7/Reals/Rdefinitions.vo theories7/Reals/Raxioms.vo theories7/Reals/RIneq.vo theories7/Reals/DiscrR.vo theories7/Reals/Rbase.vo theories7/Reals/R_Ifp.vo theories7/Reals/Rbasic_fun.vo theories7/Reals/R_sqr.vo theories7/Reals/SplitAbsolu.vo theories7/Reals/SplitRmult.vo theories7/Reals/ArithProp.vo theories7/Reals/Rfunctions.vo theories7/Reals/Rseries.vo theories7/Reals/SeqProp.vo theories7/Reals/Rcomplete.vo theories7/Reals/PartSum.vo theories7/Reals/AltSeries.vo theories7/Reals/Binomial.vo theories7/Reals/Rsigma.vo theories7/Reals/Rprod.vo theories7/Reals/Cauchy_prod.vo theories7/Reals/Alembert.vo theories7/Reals/SeqSeries.vo theories7/Reals/Rtrigo_fun.vo theories7/Reals/Rtrigo_def.vo theories7/Reals/Rtrigo_alt.vo theories7/Reals/Cos_rel.vo theories7/Reals/Cos_plus.vo theories7/Reals/Rtrigo.vo theories7/Reals/Rlimit.vo theories7/Reals/Rderiv.vo theories7/Reals/RList.vo theories7/Reals/Ranalysis1.vo theories7/Reals/Ranalysis2.vo theories7/Reals/Ranalysis3.vo theories7/Reals/Rtopology.vo theories7/Reals/MVT.vo theories7/Reals/PSeries_reg.vo theories7/Reals/Exp_prop.vo theories7/Reals/Rtrigo_reg.vo theories7/Reals/Rsqrt_def.vo theories7/Reals/R_sqrt.vo theories7/Reals/Rtrigo_calc.vo theories7/Reals/Rgeom.vo theories7/Reals/Sqrt_reg.vo theories7/Reals/Ranalysis4.vo theories7/Reals/Rpower.vo theories7/Reals/Ranalysis.vo theories7/Reals/NewtonInt.vo theories7/Reals/RiemannInt_SF.vo theories7/Reals/RiemannInt.vo theories7/Reals/Integration.vo theories7/Reals/Reals.vo theories7/Setoids/Setoid.vo theories7/Sorting/Heap.vo theories7/Sorting/Permutation.vo theories7/Sorting/Sorting.vo theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo theories7/ZArith/Zsyntax.vo theories7/ZArith/zarith_aux.vo theories7/ZArith/fast_integer.vo theories7/Reals/Rsyntax.vo contrib7/omega/OmegaLemmas.vo contrib7/omega/Omega.vo contrib7/romega/ReflOmegaCore.vo contrib7/romega/ROmega.vo contrib7/ring/ArithRing.vo contrib7/ring/Ring_normalize.vo contrib7/ring/Ring_theory.vo contrib7/ring/Ring.vo contrib7/ring/NArithRing.vo contrib7/ring/ZArithRing.vo contrib7/ring/Ring_abstract.vo contrib7/ring/Quote.vo contrib7/ring/Setoid_ring_normalize.vo contrib7/ring/Setoid_ring.vo contrib7/ring/Setoid_ring_theory.vo contrib7/field/Field_Compl.vo contrib7/field/Field_Theory.vo contrib7/field/Field_Tactic.vo contrib7/field/Field.vo contrib7/fourier/Fourier_util.vo contrib7/fourier/Fourier.vo contrib7/cc/CCSolve.vo; do \ mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/`dirname $f`; \ cp $f '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/`dirname $f`; \ done mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/states7 cp states7/*.coq '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/states7 mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq' for f in theories/Init/Notations.vo theories/Init/Datatypes.vo theories/Init/Peano.vo theories/Init/Logic.vo theories/Init/Specif.vo theories/Init/Logic_Type.vo theories/Init/Wf.vo theories/Init/Prelude.vo theories/Logic/Hurkens.vo theories/Logic/ProofIrrelevance.vo theories/Logic/Classical.vo theories/Logic/Classical_Type.vo theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo theories/Logic/ClassicalFacts.vo theories/Logic/ChoiceFacts.vo theories/Logic/Berardi.vo theories/Logic/Eqdep_dec.vo theories/Logic/Decidable.vo theories/Logic/JMeq.vo theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalChoice.vo theories/Logic/RelationalChoice.vo theories/Logic/Diaconescu.vo theories/Arith/Arith.vo theories/Arith/Gt.vo theories/Arith/Between.vo theories/Arith/Le.vo theories/Arith/Compare.vo theories/Arith/Lt.vo theories/Arith/Compare_dec.vo theories/Arith/Min.vo theories/Arith/Div2.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Even.vo theories/Arith/EqNat.vo theories/Arith/Peano_dec.vo theories/Arith/Euclid.vo theories/Arith/Plus.vo theories/Arith/Wf_nat.vo theories/Arith/Max.vo theories/Arith/Bool_nat.vo theories/Arith/Factorial.vo theories/Bool/Bool.vo theories/Bool/IfProp.vo theories/Bool/Zerob.vo theories/Bool/DecBool.vo theories/Bool/Sumbool.vo theories/Bool/BoolEq.vo theories/Bool/Bvector.vo theories/NArith/BinPos.vo theories/NArith/Pnat.vo theories/NArith/BinNat.vo theories/NArith/NArith.vo theories/ZArith/BinInt.vo theories/ZArith/Wf_Z.vo theories/ZArith/ZArith.vo theories/ZArith/ZArith_dec.vo theories/ZArith/auxiliary.vo theories/ZArith/Zmisc.vo theories/ZArith/Zcompare.vo theories/ZArith/Znat.vo theories/ZArith/Zorder.vo theories/ZArith/Zabs.vo theories/ZArith/Zmin.vo theories/ZArith/Zeven.vo theories/ZArith/Zhints.vo theories/ZArith/Zlogarithm.vo theories/ZArith/Zpower.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo theories/ZArith/Znumtheory.vo theories/Lists/MonoList.vo theories/Lists/ListSet.vo theories/Lists/Streams.vo theories/Lists/TheoryList.vo theories/Lists/List.vo theories/Sets/Classical_sets.vo theories/Sets/Permut.vo theories/Sets/Constructive_sets.vo theories/Sets/Powerset.vo theories/Sets/Cpo.vo theories/Sets/Powerset_Classical_facts.vo theories/Sets/Ensembles.vo theories/Sets/Powerset_facts.vo theories/Sets/Finite_sets.vo theories/Sets/Relations_1.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Relations_1_facts.vo theories/Sets/Image.vo theories/Sets/Relations_2.vo theories/Sets/Infinite_sets.vo theories/Sets/Relations_2_facts.vo theories/Sets/Integers.vo theories/Sets/Relations_3.vo theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo theories/IntMap/Addec.vo theories/IntMap/Mapcard.vo theories/IntMap/Addr.vo theories/IntMap/Mapc.vo theories/IntMap/Adist.vo theories/IntMap/Mapfold.vo theories/IntMap/Allmaps.vo theories/IntMap/Mapiter.vo theories/IntMap/Fset.vo theories/IntMap/Maplists.vo theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo theories/IntMap/Mapaxioms.vo theories/IntMap/Map.vo theories/Relations/Newman.vo theories/Relations/Operators_Properties.vo theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Relations.vo theories/Relations/Rstar.vo theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Wellfounded.vo theories/Wellfounded/Well_Ordering.vo theories/Wellfounded/Lexicographic_Product.vo theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/Reals/Rtrigo.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo theories/Reals/RList.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo theories/Reals/Ranalysis.vo theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo theories/Reals/Integration.vo theories/Reals/Reals.vo theories/Setoids/Setoid.vo theories/Sorting/Heap.vo theories/Sorting/Permutation.vo theories/Sorting/Sorting.vo contrib/omega/OmegaLemmas.vo contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo contrib/ring/ArithRing.vo contrib/ring/Ring_normalize.vo contrib/ring/Ring_theory.vo contrib/ring/Ring.vo contrib/ring/NArithRing.vo contrib/ring/ZArithRing.vo contrib/ring/Ring_abstract.vo contrib/ring/Quote.vo contrib/ring/Setoid_ring_normalize.vo contrib/ring/Setoid_ring.vo contrib/ring/Setoid_ring_theory.vo contrib/field/Field_Compl.vo contrib/field/Field_Theory.vo contrib/field/Field_Tactic.vo contrib/field/Field.vo contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo contrib/cc/CCSolve.vo ; do \ mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/`dirname $f`; \ cp $f '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/`dirname $f`; \ done mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/states cp states/*.coq '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/states mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/man'/man1 cp man/coq-tex.1 man/coqdep.1 man/gallina.1 man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 man/coqwc.1 man/coqdoc.1 man/coq_makefile.1 man/coqmktop.1 '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/man'/man1 mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/emacs/site-lisp/coq' cp tools/coq.el tools/coq-inferior.el '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/emacs/site-lisp/coq' mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/emacs/site-lisp' cp tools/coqdoc/coqdoc.sty '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/emacs/site-lisp' mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cp bin/coqide.byte '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cd '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin'; ln -sf coqide.byte coqide mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/ide cp ide/utf8.vo ide/utf8.v ide/coq.ico ide/coq2.ico ide/.coqide-gtk2rc '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/ide mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/ide cp ide/FAQ '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/ide mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' cp bin/coq-interface bin/parser '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin' mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/contrib/interface cp contrib/interface/vernacrc '/build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq'/contrib/interface mkdir -p '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/man'/man1 cp man/coq-interface.1 man/parser.1 '/build/buildd/coq-8.0pl3/debian/tmp/usr/share/man'/man1 make[1]: Leaving directory `/build/buildd/coq-8.0pl3' for i in /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/*.opt; do \ echo "Stripping: $i"; \ strip -R .note -R .comment $i; \ done Stripping: /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/*.opt strip: '/build/buildd/coq-8.0pl3/debian/tmp/usr/bin/*.opt': No such file for i in /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/coqide.*; do \ echo "Rpath for `chrpath $i`"; \ echo "Removing rpath: $i"; \ chrpath -d $i; \ done Rpath for /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/coqide.byte: no rpath or runpath tag found. Removing rpath: /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/coqide.byte cp debian/coq.xpm debian/coq/usr/share/pixmaps/coq.xpm cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm cp debian/coqide.desktop debian/coqide/usr/share/applications cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt if [ -e opt-stamp ]; then \ cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \ cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \ fi cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.1 cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.byte.1 cp debian/coqc.1 debian/coq/usr/share/man/man1/coqc.1 cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.1 cp debian/coq_makefile.1 debian/coq/usr/share/man/man1/coq_makefile.1 cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1 cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1 chmod -x debian/tmp/usr/lib/coq/ide/coq2.ico # These are installed as docs rm -f /build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq/ide/utf8.v /build/buildd/coq-8.0pl3/debian/tmp/usr/lib/coq/ide/FAQ dh_install --sourcedir=/build/buildd/coq-8.0pl3/debian/tmp --list-missing dh_install: /build/buildd/coq-8.0pl3/debian/tmp/usr/bin/parser exists in debian/tmp but is not installed to anywhere dh_install: /build/buildd/coq-8.0pl3/debian/tmp/usr/share/man/man1/parser.1 exists in debian/tmp but is not installed to anywhere /usr/bin/make -f debian/rules DH_OPTIONS=-a binary-common make[1]: Entering directory `/build/buildd/coq-8.0pl3' dh_testdir dh_testroot dh_installdocs dh_installmenu dh_installemacsen dh_installman dh_installchangelogs CHANGES dh_desktop dh_link dh_compress dh_fixperms dh_installdeb dh_shlibdeps dh_gencontrol dh_md5sums dh_builddeb pkgstriptranslations: processing control file: ./debian/coq/DEBIAN/control, package coq, directory ./debian/coq pkgstriptranslations: coq does not contain translations, skipping pkgstriptranslations: processing control file: ./debian/coqide/DEBIAN/control, package coqide, directory ./debian/coqide pkgstriptranslations: coqide does not contain translations, skipping pkgstriptranslations: no translation files, not creating tarball tar: -: file name read contains nul character dpkg-deb: building package `coq' in `../coq_8.0pl3-2_ia64.deb'. pkgstriptranslations: processing control file: ./debian/coq/DEBIAN/control, package coq, directory ./debian/coq pkgstriptranslations: coq does not contain translations, skipping pkgstriptranslations: processing control file: ./debian/coqide/DEBIAN/control, package coqide, directory ./debian/coqide pkgstriptranslations: coqide does not contain translations, skipping pkgstriptranslations: no translation files, not creating tarball tar: -: file name read contains nul character dpkg-deb: building package `coqide' in `../coqide_8.0pl3-2_ia64.deb'. make[1]: Leaving directory `/build/buildd/coq-8.0pl3' dpkg-genchanges -B -mUbuntu/ia64 Build Daemon dpkg-genchanges: arch-specific upload - not including arch-independent packages dpkg-genchanges: binary-only upload - not including any source code dpkg-buildpackage: binary only upload (no source included) ****************************************************************************** Build finished at 20060708-1314 chroot-autobuild/build/buildd/coq_8.0pl3-2_ia64.deb: new debian package, version 2.0. size 3146584 bytes: control archive= 2000 bytes. 33 bytes, 1 lines conffiles 972 bytes, 22 lines control 2126 bytes, 34 lines md5sums 403 bytes, 13 lines * postinst #!/bin/sh 160 bytes, 5 lines * postrm #!/bin/sh 209 bytes, 7 lines * prerm #!/bin/sh Package: coq Version: 8.0pl3-2 Section: math Priority: optional Architecture: ia64 Depends: libc6.1 (>= 2.4-1), libncurses5 (>= 5.4-5), coq-libs (= 8.0pl3-2) Recommends: coqide | proofgeneral-coq Suggests: ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle Installed-Size: 14048 Maintainer: Debian OCaml Maintainers Description: proof assistant for higher-order logic (toplevel and compiler) Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp4. For more information, see . . This packages provides coqtop, a command line interface to Coq. . A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral-coq package to be installed. chroot-autobuild/build/buildd/coqide_8.0pl3-2_ia64.deb: new debian package, version 2.0. size 1397762 bytes: control archive= 1406 bytes. 912 bytes, 17 lines control 1014 bytes, 16 lines md5sums 368 bytes, 12 lines * postinst #!/bin/sh 340 bytes, 10 lines * postrm #!/bin/sh Package: coqide Version: 8.0pl3-2 Section: math Priority: optional Architecture: ia64 Depends: libatk1.0-0 (>= 1.9.0), libc6.1 (>= 2.4-1), libcairo2 (>= 1.2.0), libfontconfig1 (>= 2.3.0), libglib2.0-0 (>= 2.10.0), libgtk2.0-0 (>= 2.8.0), libncurses5 (>= 5.4-5), libpango1.0-0 (>= 1.13.2), libx11-6, libxcursor1 (>> 1.1.2), libxext6, libxfixes3, libxi6, libxinerama1, libxrandr2, libxrender1, coq (>= 8.0) Installed-Size: 6744 Maintainer: Debian OCaml Maintainers Source: coq Description: proof assistant for higher-order logic (gtk interface) Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp4. For more information, see . . This package provides CoqIde, a graphical user interface for developing proofs. chroot-autobuild/build/buildd/coq_8.0pl3-2_ia64.deb: drwxr-xr-x root/root 0 2006-07-08 13:13:49 ./ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/ drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/bin/ -rwxr-xr-x root/root 539446 2006-07-08 13:13:42 ./usr/bin/coqc -rwxr-xr-x root/root 576501 2006-07-08 13:13:42 ./usr/bin/coqdep -rwxr-xr-x root/root 720802 2006-07-08 13:13:42 ./usr/bin/coqdoc -rwxr-xr-x root/root 5098280 2006-07-08 13:13:46 ./usr/bin/coq-interface -rwxr-xr-x root/root 430519 2006-07-08 13:13:42 ./usr/bin/coq_makefile -rwxr-xr-x root/root 577862 2006-07-08 13:13:42 ./usr/bin/coqmktop -rwxr-xr-x root/root 460514 2006-07-08 13:13:42 ./usr/bin/coq-tex -rwxr-xr-x root/root 4833583 2006-07-08 13:13:42 ./usr/bin/coqtop.byte -rwxr-xr-x root/root 410653 2006-07-08 13:13:42 ./usr/bin/coqwc -rwxr-xr-x root/root 421530 2006-07-08 13:13:42 ./usr/bin/gallina drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/lib/ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/lib/coq/ drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/lib/emacsen-common/ drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/lib/emacsen-common/packages/ drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/lib/emacsen-common/packages/install/ -rwxr-xr-x root/root 1227 2006-07-08 13:13:47 ./usr/lib/emacsen-common/packages/install/coq drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/lib/emacsen-common/packages/remove/ -rwxr-xr-x root/root 453 2006-07-08 13:13:47 ./usr/lib/emacsen-common/packages/remove/coq drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/share/ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/share/man/ drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/share/man/man1/ -rw-r--r-- root/root 320 2006-07-08 13:13:46 ./usr/share/man/man1/coq_makefile.1.gz -rw-r--r-- root/root 453 2006-07-08 13:13:46 ./usr/share/man/man1/coqmktop.1.gz -rw-r--r-- root/root 379 2006-07-08 13:13:46 ./usr/share/man/man1/coqtop.1.gz -rw-r--r-- root/root 1264 2006-07-08 13:13:46 ./usr/share/man/man1/coq-tex.1.gz -rw-r--r-- root/root 1431 2006-07-08 13:13:46 ./usr/share/man/man1/coqdep.1.gz -rw-r--r-- root/root 325 2006-07-08 13:13:46 ./usr/share/man/man1/coqdoc.1.gz -rw-r--r-- root/root 292 2006-07-08 13:13:46 ./usr/share/man/man1/coqtop.opt.1.gz -rw-r--r-- root/root 320 2006-07-08 13:13:46 ./usr/share/man/man1/coqwc.1.gz -rw-r--r-- root/root 663 2006-07-08 13:13:46 ./usr/share/man/man1/gallina.1.gz -rw-r--r-- root/root 475 2006-07-08 13:13:46 ./usr/share/man/man1/coqc.1.gz -rw-r--r-- root/root 372 2006-07-08 13:13:46 ./usr/share/man/man1/coq-interface.1.gz -rw-r--r-- root/root 289 2006-07-08 13:13:46 ./usr/share/man/man1/coqtop.byte.1.gz drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/pixmaps/ -rw-r--r-- root/root 1496 2006-07-08 13:13:46 ./usr/share/pixmaps/coq.xpm drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/emacs/ drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/emacs/site-lisp/ drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/emacs/site-lisp/coq/ -rw-r--r-- root/root 7010 2006-07-08 13:13:46 ./usr/share/emacs/site-lisp/coq/coq.el -rw-r--r-- root/root 11606 2006-07-08 13:13:46 ./usr/share/emacs/site-lisp/coq/coq-inferior.el -rw-r--r-- root/root 1642 2006-07-08 13:13:46 ./usr/share/emacs/site-lisp/coqdoc.sty drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/share/doc/ drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/share/doc/coq/ -rw-r--r-- root/root 2445 2004-07-16 20:30:21 ./usr/share/doc/coq/utf8.v -rw-r--r-- root/root 1685 2006-07-08 12:26:46 ./usr/share/doc/coq/README.Debian -rw-r--r-- root/root 1949 2006-07-08 12:26:46 ./usr/share/doc/coq/copyright -rw-r--r-- root/root 16323 2006-01-11 17:27:26 ./usr/share/doc/coq/changelog.gz -rw-r--r-- root/root 3227 2006-07-08 12:26:46 ./usr/share/doc/coq/changelog.Debian.gz drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/share/menu/ -rw-r--r-- root/root 131 2006-07-08 12:26:46 ./usr/share/menu/coq drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./etc/ drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./etc/emacs/ drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./etc/emacs/site-start.d/ -rw-r--r-- root/root 851 2006-07-08 13:13:47 ./etc/emacs/site-start.d/50coq.el lrwxrwxrwx root/root 0 2006-07-08 13:13:48 ./usr/bin/coqtop -> coqtop.byte chroot-autobuild/build/buildd/coqide_8.0pl3-2_ia64.deb: drwxr-xr-x root/root 0 2006-07-08 13:13:49 ./ drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/lib/ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/lib/coq/ drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/lib/coq/ide/ -rw-r--r-- root/root 21782 2006-07-08 13:13:46 ./usr/lib/coq/ide/index_urls.txt -rw-r--r-- root/root 96774 2006-07-08 13:13:46 ./usr/lib/coq/ide/coq.ico -rw-r--r-- root/root 1526 2006-07-08 13:13:46 ./usr/lib/coq/ide/coq2.ico -rw-r--r-- root/root 4936 2006-07-08 13:13:46 ./usr/lib/coq/ide/utf8.vo -rw-r--r-- root/root 1127 2006-07-08 13:13:46 ./usr/lib/coq/ide/.coqide-gtk2rc drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/share/ drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/share/doc/ drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/share/doc/coqide/ -rw-r--r-- root/root 3157 2004-01-20 15:16:45 ./usr/share/doc/coqide/FAQ -rw-r--r-- root/root 2445 2004-07-16 20:30:21 ./usr/share/doc/coqide/utf8.v -rw-r--r-- root/root 1949 2006-07-08 12:26:46 ./usr/share/doc/coqide/copyright -rw-r--r-- root/root 16323 2006-01-11 17:27:26 ./usr/share/doc/coqide/changelog.gz -rw-r--r-- root/root 3227 2006-07-08 12:26:46 ./usr/share/doc/coqide/changelog.Debian.gz drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/applications/ -rw-r--r-- root/root 213 2006-07-08 13:13:46 ./usr/share/applications/coqide.desktop drwxr-xr-x root/root 0 2006-07-08 13:13:41 ./usr/share/man/ drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/share/man/man1/ -rw-r--r-- root/root 1155 2006-07-08 13:13:46 ./usr/share/man/man1/coqide.1.gz -rw-r--r-- root/root 1160 2006-07-08 13:13:46 ./usr/share/man/man1/coqide.byte.1.gz drwxr-xr-x root/root 0 2006-07-08 13:13:46 ./usr/share/pixmaps/ -rw-r--r-- root/root 1496 2006-07-08 13:13:46 ./usr/share/pixmaps/coqide.xpm drwxr-xr-x root/root 0 2006-07-08 13:13:47 ./usr/share/menu/ -rw-r--r-- root/root 139 2006-07-08 12:26:46 ./usr/share/menu/coqide drwxr-xr-x root/root 0 2006-07-08 13:13:48 ./usr/bin/ -rwxr-xr-x root/root 6623318 2006-07-08 13:13:46 ./usr/bin/coqide.byte lrwxrwxrwx root/root 0 2006-07-08 13:13:48 ./usr/bin/coqide -> coqide.byte coq_8.0pl3-2_ia64.changes: Format: 1.7 Date: Sun, 19 Feb 2006 11:33:21 +0000 Source: coq Binary: coq7-libs coqide coq-libs coq Architecture: ia64 Version: 8.0pl3-2 Distribution: autobuild Urgency: low Maintainer: Ubuntu/ia64 Build Daemon Changed-By: Samuel Mimram Description: coq - proof assistant for higher-order logic (toplevel and compiler) coqide - proof assistant for higher-order logic (gtk interface) Closes: 353493 Changes: coq (8.0pl3-2) unstable; urgency=low . * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from looping forever, closes: #353493. Files: 34c4b93111f930c578c2577a7e2bb4d9 3146584 math optional coq_8.0pl3-2_ia64.deb 69283bc2dfa56b377ddd65dcb5da66a6 1397762 math optional coqide_8.0pl3-2_ia64.deb ****************************************************************************** Built successfully Purging chroot-autobuild/build/buildd/coq-8.0pl3 ------------------------------------------------------------------------------ /usr/bin/sudo dpkg --root=/srv/hooker.ubuntu.com/home/buildd/build-212105-157183/chroot-autobuild --purge libxfixes-dev libx11-data libxdmcp-dev defoma readline-common gettext file zlib1g-dev libcairo2-dev ttf-dejavu fontconfig libcairo2 x11-common libx11-dev libxi6 libpopt0 chrpath libfreetype6 libjpeg62 libssl0.9.8 libatk1.0-0 x11proto-fixes-dev libxcursor1 libfreetype6-dev libgtk2.0-0 ocaml-interp x11proto-input-dev tk8.4 libexpat1-dev libgtk2.0-bin ocaml libgtkspell-dev html2text libglade2-0 libxrandr2 debhelper libfontconfig1 ocaml-base-nox python libncurses5-dev ocaml-native-compilers ocaml-nox libmagic1 libtiff4 libexpat1 libxau6 libpango1.0-dev libglade2-dev libxcursor-dev libx11-6 xtrans-dev x11proto-randr-dev libglib2.0-0 mime-support liblablgtk2-ocaml libnewt0.52 x11proto-core-dev libxinerama-dev whiptail libpango1.0-common dpatch libxi-dev libxdmcp6 libxfixes3 libgtk2.0-dev po-debconf libglib2.0-dev ttf-bitstream-vera libatk1.0-dev liblablgtk2-ocaml-dev ocaml-base libxft-dev libxml2 x11proto-xext-dev pkg-config libpng12-0 libaspell-dev x11proto-kb-dev intltool-debian x11proto-xinerama-dev libxrender1 libgtkspell0 libfontconfig1-dev libxml2-dev libxrandr-dev libpango1.0-0 libxext-dev python2.4 ucf ttf-freefont libxau-dev libgtk2.0-common libaspell15 libxrender-dev gettext-base libpng12-dev libreadline5 libxft2 x11proto-render-dev libxext6 libbz2-1.0 libxinerama1 tcl8.4 libncursesw5 (Reading database ... 15716 files and directories currently installed.) Removing chrpath ... Removing debhelper ... Removing ocaml-native-compilers ... Removing dpatch ... Purging configuration files for dpatch ... Removing po-debconf ... Removing liblablgtk2-ocaml-dev ... Removing intltool-debian ... Removing gettext ... Removing ocaml ... Purging configuration files for ocaml ... Removing libgtkspell-dev ... Removing html2text ... Purging configuration files for html2text ... Removing ocaml-nox ... Purging configuration files for ocaml-nox ... Removing libglade2-dev ... dpkg - warning: while removing libglade2-dev, directory `/usr/share/gtk-doc/html/libglade' not empty so not removed. dpkg - warning: while removing libglade2-dev, directory `/usr/share/gtk-doc/html' not empty so not removed. dpkg - warning: while removing libglade2-dev, directory `/usr/share/gtk-doc' not empty so not removed. dpkg - warning: while removing libglade2-dev, directory `/usr/share/doc/libglade2-dev' not empty so not removed. Removing liblablgtk2-ocaml ... Removing libgtk2.0-dev ... Removing libatk1.0-dev ... Removing ocaml-base ... dpkg - warning: while removing ocaml-base, directory `/usr/share/doc/ocaml-base' not empty so not removed. Removing libaspell-dev ... Removing libgtkspell0 ... Purging configuration files for libgtkspell0 ... Removing libxml2-dev ... Removing libxrandr-dev ... Removing libaspell15 ... Purging configuration files for libaspell15 ... Removing gettext-base ... Removing ocaml-interp ... Purging configuration files for ocaml-interp ... Removing tk8.4 ... Purging configuration files for tk8.4 ... Removing libglade2-0 ... Purging configuration files for libglade2-0 ... Removing ocaml-base-nox ... Removing python ... Removing libncurses5-dev ... Removing libpango1.0-dev ... Removing libxcursor-dev ... Removing x11proto-randr-dev ... Removing libxinerama-dev ... Removing libxi-dev ... Removing libglib2.0-dev ... Removing libxft-dev ... Removing libxml2 ... Purging configuration files for libxml2 ... Removing x11proto-xinerama-dev ... Removing python2.4 ... Purging configuration files for python2.4 ... Removing libreadline5 ... Purging configuration files for libreadline5 ... Removing libbz2-1.0 ... Purging configuration files for libbz2-1.0 ... Removing tcl8.4 ... Purging configuration files for tcl8.4 ... Removing libncursesw5 ... Purging configuration files for libncursesw5 ... Removing libxfixes-dev ... Removing readline-common ... Purging configuration files for readline-common ... Removing libcairo2-dev ... Removing libssl0.9.8 ... Purging configuration files for libssl0.9.8 ... Removing x11proto-fixes-dev ... Removing mime-support ... Purging configuration files for mime-support ... Removing libfontconfig1-dev ... Removing libxrender-dev ... Removing libpng12-dev ... Removing x11proto-render-dev ... Removing libfreetype6-dev ... Removing libexpat1-dev ... Removing pkg-config ... Removing zlib1g-dev ... Removing libx11-dev ... Removing xtrans-dev ... Removing x11proto-kb-dev ... Removing libxext-dev ... Removing libxdmcp-dev ... Removing libgtk2.0-0 ... Purging configuration files for libgtk2.0-0 ... Removing libgtk2.0-bin ... Purging configuration files for libgtk2.0-bin ... Removing libxrandr2 ... Purging configuration files for libxrandr2 ... Removing libtiff4 ... Purging configuration files for libtiff4 ... Removing libpango1.0-common ... Purging font configuration of pango... Purging category xfont.. Purging configuration files for libpango1.0-common ... Removing x11proto-xext-dev ... Removing libpango1.0-0 ... Purging configuration files for libpango1.0-0 ... Removing libxau-dev ... Removing libgtk2.0-common ... Removing libxft2 ... Purging configuration files for libxft2 ... Removing libxinerama1 ... Purging configuration files for libxinerama1 ... Removing fontconfig ... Purging font configuration of fontconfig... Purging category cid.. Purging category truetype.. Purging category type1.. Purging configuration files for fontconfig ... dpkg - warning: while removing fontconfig, directory `/etc/fonts/conf.d' not empty so not removed. dpkg - warning: while removing fontconfig, directory `/etc/fonts' not empty so not removed. Removing libcairo2 ... Purging configuration files for libcairo2 ... Removing libxi6 ... Purging configuration files for libxi6 ... Removing libjpeg62 ... Removing libatk1.0-0 ... Purging configuration files for libatk1.0-0 ... Removing libxcursor1 ... Purging configuration files for libxcursor1 ... Removing x11proto-input-dev ... Removing libfontconfig1 ... Purging configuration files for libfontconfig1 ... Removing libexpat1 ... Purging configuration files for libexpat1 ... Removing libglib2.0-0 ... Purging configuration files for libglib2.0-0 ... Removing x11proto-core-dev ... Removing libxfixes3 ... Purging configuration files for libxfixes3 ... Removing ttf-bitstream-vera ... Purging configuration files for ttf-bitstream-vera ... Removing libpng12-0 ... Purging configuration files for libpng12-0 ... Removing libxrender1 ... Purging configuration files for libxrender1 ... Removing ucf ... Purging configuration files for ucf ... find: /var/lib/ucf/cache: No such file or directory rmdir: /var/lib/ucf/cache: No such file or directory Removing ttf-freefont ... Purging configuration files for ttf-freefont ... Removing libxext6 ... Purging configuration files for libxext6 ... Removing ttf-dejavu ... Purging configuration files for ttf-dejavu ... dpkg - warning: while removing ttf-dejavu, directory `/usr/share/fonts' not empty so not removed. Removing libfreetype6 ... Purging configuration files for libfreetype6 ... Removing libx11-6 ... Purging configuration files for libx11-6 ... Removing libxdmcp6 ... Purging configuration files for libxdmcp6 ... Removing libx11-data ... Removing defoma ... Purging configuration files for defoma ... dpkg - warning: while removing defoma, directory `/etc/defoma' not empty so not removed. Removing file ... Purging configuration files for file ... Removing libmagic1 ... Purging configuration files for libmagic1 ... Removing libxau6 ... Purging configuration files for libxau6 ... Removing whiptail ... Removing x11-common ... Purging configuration files for x11-common ... dpkg - warning: while removing x11-common, directory `/usr/X11R6' not empty so not removed. dpkg - warning: while removing x11-common, directory `/usr/share/X11' not empty so not removed. Removing libpopt0 ... Purging configuration files for libpopt0 ... Removing libnewt0.52 ... Purging configuration files for libnewt0.52 ... ****************************************************************************** Finished at 20060708-1315 Build needed 00:48:05, 145144k disk space RUN: /usr/share/launchpad-buildd/slavebin/scan-for-processes ['/usr/share/launchpad-buildd/slavebin/scan-for-processes', '212105-157183'] Scanning for processes to kill in build 212105-157183... Scanning for processes to kill in build /home/buildd/build-212105-157183/chroot-autobuild... RUN: /usr/share/launchpad-buildd/slavebin/umount-chroot ['umount-chroot', '212105-157183'] Unmounting chroot for build 212105-157183... RUN: /usr/share/launchpad-buildd/slavebin/remove-build ['remove-build', '212105-157183'] Removing build 212105-157183