RUN: /usr/share/launchpad-buildd/slavebin/slave-prep ['slave-prep'] Forking launchpad-buildd slave process... Kernel version: 3.2.0-23-generic #36-Ubuntu SMP Tue Apr 10 20:39:51 UTC 2012 x86_64 Buildd toolchain package versions: launchpad-buildd_114-0~53~0.IS.08.04 python-lpbuildd_114-0~53~0.IS.08.04 bzr_2.5.0-2ubuntu2. Syncing the system clock with the buildd NTP service... 2 May 07:31:28 ntpdate[8235]: adjust time server 10.211.37.1 offset 0.000001 sec RUN: /usr/share/launchpad-buildd/slavebin/unpack-chroot ['unpack-chroot', '9c515e1d21eaaf895970634411847f687b65d982', '/home/buildd/filecache-default/5361914ad95ed65786be6b5cbe332850c615ec0e'] Unpacking chroot for build 9c515e1d21eaaf895970634411847f687b65d982 RUN: /usr/share/launchpad-buildd/slavebin/mount-chroot ['mount-chroot', '9c515e1d21eaaf895970634411847f687b65d982'] Mounting chroot for build 9c515e1d21eaaf895970634411847f687b65d982 RUN: /usr/share/launchpad-buildd/slavebin/override-sources-list ['override-sources-list', '9c515e1d21eaaf895970634411847f687b65d982', 'deb http://ftpmaster.internal/ubuntu quantal main restricted universe multiverse'] Overriding sources.list in build-9c515e1d21eaaf895970634411847f687b65d982 RUN: /usr/share/launchpad-buildd/slavebin/update-debian-chroot ['update-debian-chroot', '9c515e1d21eaaf895970634411847f687b65d982', 'i386'] Updating debian chroot for build 9c515e1d21eaaf895970634411847f687b65d982 Ign http://ftpmaster.internal quantal InRelease Get:1 http://ftpmaster.internal quantal Release.gpg [198 B] Get:2 http://ftpmaster.internal quantal Release [49.6 kB] Get:3 http://ftpmaster.internal quantal/main i386 Packages [1313 kB] Get:4 http://ftpmaster.internal quantal/restricted i386 Packages [8394 B] Get:5 http://ftpmaster.internal quantal/universe i386 Packages [4857 kB] Get:6 http://ftpmaster.internal quantal/multiverse i386 Packages [121 kB] Get:7 http://ftpmaster.internal quantal/main TranslationIndex [74 B] Get:8 http://ftpmaster.internal quantal/multiverse TranslationIndex [73 B] Get:9 http://ftpmaster.internal quantal/restricted TranslationIndex [72 B] Get:10 http://ftpmaster.internal quantal/universe TranslationIndex [75 B] Get:11 http://ftpmaster.internal quantal/main Translation-en [740 kB] Get:12 http://ftpmaster.internal quantal/multiverse Translation-en [93.2 kB] Get:13 http://ftpmaster.internal quantal/restricted Translation-en [2395 B] Get:14 http://ftpmaster.internal quantal/universe Translation-en [3371 kB] Fetched 10.6 MB in 4s (2332 kB/s) Reading package lists... Reading package lists... Building dependency tree... Reading state information... The following packages will be upgraded: coreutils cpp-4.7 g++-4.7 gcc-4.7 gcc-4.7-base libgcc1 libgomp1 libgpg-error0 libitm1 libquadmath0 libssl1.0.0 libstdc++6 libstdc++6-4.7-dev linux-libc-dev openssl 15 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. Need to get 26.3 MB of archives. After this operation, 129 kB of additional disk space will be used. WARNING: The following packages cannot be authenticated! coreutils libitm1 libgomp1 gcc-4.7-base libstdc++6 cpp-4.7 libquadmath0 libstdc++6-4.7-dev g++-4.7 gcc-4.7 libgcc1 libssl1.0.0 libgpg-error0 openssl linux-libc-dev Authentication warning overridden. Get:1 http://ftpmaster.internal/ubuntu/ quantal/main coreutils i386 8.13-3.1ubuntu1 [2193 kB] Get:2 http://ftpmaster.internal/ubuntu/ quantal/main libitm1 i386 4.7.0-7ubuntu1 [35.6 kB] Get:3 http://ftpmaster.internal/ubuntu/ quantal/main libgomp1 i386 4.7.0-7ubuntu1 [29.8 kB] Get:4 http://ftpmaster.internal/ubuntu/ quantal/main gcc-4.7-base i386 4.7.0-7ubuntu1 [15.6 kB] Get:5 http://ftpmaster.internal/ubuntu/ quantal/main libstdc++6 i386 4.7.0-7ubuntu1 [336 kB] Get:6 http://ftpmaster.internal/ubuntu/ quantal/main cpp-4.7 i386 4.7.0-7ubuntu1 [5190 kB] Get:7 http://ftpmaster.internal/ubuntu/ quantal/main libquadmath0 i386 4.7.0-7ubuntu1 [198 kB] Get:8 http://ftpmaster.internal/ubuntu/ quantal/main libstdc++6-4.7-dev i386 4.7.0-7ubuntu1 [1703 kB] Get:9 http://ftpmaster.internal/ubuntu/ quantal/main g++-4.7 i386 4.7.0-7ubuntu1 [5610 kB] Get:10 http://ftpmaster.internal/ubuntu/ quantal/main gcc-4.7 i386 4.7.0-7ubuntu1 [8498 kB] Get:11 http://ftpmaster.internal/ubuntu/ quantal/main libgcc1 i386 1:4.7.0-7ubuntu1 [53.4 kB] Get:12 http://ftpmaster.internal/ubuntu/ quantal/main libssl1.0.0 i386 1.0.1-4ubuntu5 [1004 kB] Get:13 http://ftpmaster.internal/ubuntu/ quantal/main libgpg-error0 i386 1.10-3 [14.5 kB] Get:14 http://ftpmaster.internal/ubuntu/ quantal/main openssl i386 1.0.1-4ubuntu5 [519 kB] Get:15 http://ftpmaster.internal/ubuntu/ quantal/main linux-libc-dev i386 3.4.0-1.2 [862 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 26.3 MB in 1s (18.0 MB/s) (Reading database ... 12288 files and directories currently installed.) Preparing to replace coreutils 8.13-3ubuntu3 (using .../coreutils_8.13-3.1ubuntu1_i386.deb) ... Unpacking replacement coreutils ... Setting up coreutils (8.13-3.1ubuntu1) ... (Reading database ... 12288 files and directories currently installed.) Preparing to replace libitm1 4.7.0-5ubuntu1 (using .../libitm1_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libitm1 ... Preparing to replace libgomp1 4.7.0-5ubuntu1 (using .../libgomp1_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libgomp1 ... Preparing to replace gcc-4.7-base 4.7.0-5ubuntu1 (using .../gcc-4.7-base_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement gcc-4.7-base ... Setting up gcc-4.7-base (4.7.0-7ubuntu1) ... (Reading database ... 12288 files and directories currently installed.) Preparing to replace libstdc++6 4.7.0-5ubuntu1 (using .../libstdc++6_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libstdc++6 ... Setting up libstdc++6 (4.7.0-7ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 12288 files and directories currently installed.) Preparing to replace cpp-4.7 4.7.0-5ubuntu1 (using .../cpp-4.7_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement cpp-4.7 ... Preparing to replace libquadmath0 4.7.0-5ubuntu1 (using .../libquadmath0_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libquadmath0 ... Preparing to replace libstdc++6-4.7-dev 4.7.0-5ubuntu1 (using .../libstdc++6-4.7-dev_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libstdc++6-4.7-dev ... Preparing to replace g++-4.7 4.7.0-5ubuntu1 (using .../g++-4.7_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement g++-4.7 ... Preparing to replace gcc-4.7 4.7.0-5ubuntu1 (using .../gcc-4.7_4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement gcc-4.7 ... Preparing to replace libgcc1 1:4.7.0-5ubuntu1 (using .../libgcc1_1%3a4.7.0-7ubuntu1_i386.deb) ... Unpacking replacement libgcc1 ... Setting up libgcc1 (1:4.7.0-7ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 12288 files and directories currently installed.) Preparing to replace libssl1.0.0 1.0.1-4ubuntu3 (using .../libssl1.0.0_1.0.1-4ubuntu5_i386.deb) ... Unpacking replacement libssl1.0.0 ... Setting up libssl1.0.0 (1.0.1-4ubuntu5) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place (Reading database ... 12288 files and directories currently installed.) Preparing to replace libgpg-error0 1.10-2ubuntu1 (using .../libgpg-error0_1.10-3_i386.deb) ... Unpacking replacement libgpg-error0 ... Preparing to replace openssl 1.0.1-4ubuntu3 (using .../openssl_1.0.1-4ubuntu5_i386.deb) ... Unpacking replacement openssl ... Preparing to replace linux-libc-dev 3.2.0-24.37 (using .../linux-libc-dev_3.4.0-1.2_i386.deb) ... Unpacking replacement linux-libc-dev ... Setting up libitm1 (4.7.0-7ubuntu1) ... Setting up libgomp1 (4.7.0-7ubuntu1) ... Setting up cpp-4.7 (4.7.0-7ubuntu1) ... Setting up libquadmath0 (4.7.0-7ubuntu1) ... Setting up gcc-4.7 (4.7.0-7ubuntu1) ... Setting up libgpg-error0 (1.10-3) ... Setting up openssl (1.0.1-4ubuntu5) ... Setting up linux-libc-dev (3.4.0-1.2) ... Setting up g++-4.7 (4.7.0-7ubuntu1) ... Setting up libstdc++6-4.7-dev (4.7.0-7ubuntu1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place RUN: /usr/share/launchpad-buildd/slavebin/sbuild-package ['sbuild-package', '9c515e1d21eaaf895970634411847f687b65d982', 'i386', 'quantal', '--nolog', '--batch', '--archive=ubuntu', '--dist=quantal', '-A', '--purpose=PRIMARY', '--architecture=i386', '--comp=multiverse', 'coq-doc_8.3pl4-1.dsc'] Initiating build 9c515e1d21eaaf895970634411847f687b65d982 with 8 jobs across 8 processor cores. Kernel reported to sbuild: 3.2.0-23-generic #36-Ubuntu SMP Tue Apr 10 20:39:51 UTC 2012 i686 Automatic build of coq-doc_8.3pl4-1 on panlong by sbuild/i386 1.170.5 Build started at 20120502-0732 ****************************************************************************** coq-doc_8.3pl4-1.dsc exists in cwd ** Using build dependencies supplied by package: Build-Depends: debhelper (>= 8) Build-Depends-Indep: texlive, texlive-base, texlive-latex-extra, texlive-math-extra, texlive-lang-french, texlive-humanities, hevea (>= 1.05), camlp5, ocaml-nox Checking for already installed source dependencies... debhelper: missing texlive: missing texlive-base: missing texlive-latex-extra: missing texlive-math-extra: missing texlive-lang-french: missing texlive-humanities: missing hevea: missing camlp5: missing ocaml-nox: missing Checking for source dependency conflicts... /usr/bin/sudo /usr/bin/apt-get --purge $CHROOT_OPTIONS -q -y install debhelper texlive texlive-base texlive-latex-extra texlive-math-extra texlive-lang-french texlive-humanities hevea camlp5 ocaml-nox Reading package lists... Building dependency tree... Reading state information... The following extra packages will be installed: bsdmainutils dh-apparmor ed file fontconfig-config gettext gettext-base ghostscript groff-base gs-cjk-resource gsfonts html2text intltool-debian libavahi-client3 libavahi-common-data libavahi-common3 libcroco3 libcups2 libcupsimage2 libexpat1 libfontconfig1 libfreetype6 libgettextpo0 libgraphite3 libgs9 libgs9-common libice6 libijs-0.35 libjasper1 libjbig2dec0 libjpeg-turbo8 libjpeg8 libkpathsea6 liblcms2-2 libmagic1 libncurses5-dev libnetpbm10 libpaper-utils libpaper1 libpipeline1 libpoppler19 libptexenc1 libsm6 libtiff4 libtinfo-dev libunistring0 libx11-6 libx11-data libxau6 libxaw7 libxcb1 libxdmcp6 libxext6 libxml2 libxmu6 libxpm4 libxt6 luatex man-db mime-support netpbm ocaml-base-nox ocaml-compiler-libs ocaml-interp po-debconf preview-latex-style tex-common texlive-binaries texlive-common texlive-doc-base texlive-fonts-recommended texlive-latex-base texlive-latex-recommended texlive-pictures ttf-dejavu-core ttf-marvosym ucf x11-common Suggested packages: wamerican wordlist whois vacation ocaml-findlib dh-make gettext-doc ghostscript-cups ghostscript-x hpijs groff fonts-ipafont-mincho fonts-ipafont-gothic ttf-arphic-ukai ttf-arphic-uming fonts-unfonts-core hevea-doc cups-common libjasper-runtime liblcms2-utils ncurses-doc poppler-data less www-browser ocaml-doc libgdbm-dev tuareg-mode ocaml-mode libmail-box-perl texlive-doc-en perl-tk xpdf-reader pdf-viewer gv postscript-viewer libfile-which-perl texpower dot2tex Recommended packages: curl wget lynx-cur cmap-adobe-japan1 cmap-adobe-cns1 cmap-adobe-gb1 cmap-adobe-korea1 cmap-adobe-japan2 xml-core texlive-luatex ledit readline-editor camlp4 libmail-sendmail-perl doc-base lmodern python ruby wish texlive-fonts-recommended-doc tex-gyre tipa texlive-humanities-doc texlive-latex-base-doc texlive-latex-extra-doc latex-xcolor texlive-latex-recommended-doc prosper latex-beamer texlive-pictures-doc pgf The following NEW packages will be installed: bsdmainutils camlp5 debhelper dh-apparmor ed file fontconfig-config gettext gettext-base ghostscript groff-base gs-cjk-resource gsfonts hevea html2text intltool-debian libavahi-client3 libavahi-common-data libavahi-common3 libcroco3 libcups2 libcupsimage2 libexpat1 libfontconfig1 libfreetype6 libgettextpo0 libgraphite3 libgs9 libgs9-common libice6 libijs-0.35 libjasper1 libjbig2dec0 libjpeg-turbo8 libjpeg8 libkpathsea6 liblcms2-2 libmagic1 libncurses5-dev libnetpbm10 libpaper-utils libpaper1 libpipeline1 libpoppler19 libptexenc1 libsm6 libtiff4 libtinfo-dev libunistring0 libx11-6 libx11-data libxau6 libxaw7 libxcb1 libxdmcp6 libxext6 libxml2 libxmu6 libxpm4 libxt6 luatex man-db mime-support netpbm ocaml-base-nox ocaml-compiler-libs ocaml-interp ocaml-nox po-debconf preview-latex-style tex-common texlive texlive-base texlive-binaries texlive-common texlive-doc-base texlive-fonts-recommended texlive-humanities texlive-lang-french texlive-latex-base texlive-latex-extra texlive-latex-recommended texlive-math-extra texlive-pictures ttf-dejavu-core ttf-marvosym ucf x11-common 0 upgraded, 88 newly installed, 0 to remove and 0 not upgraded. Need to get 121 MB of archives. After this operation, 308 MB of additional disk space will be used. WARNING: The following packages cannot be authenticated! libexpat1 libmagic1 libpipeline1 libxau6 libxdmcp6 libxcb1 libx11-data libx11-6 libxext6 libxml2 libavahi-common-data libavahi-common3 libavahi-client3 libcroco3 libcups2 libjpeg-turbo8 libjpeg8 libtiff4 libcupsimage2 libfreetype6 ucf ttf-dejavu-core fontconfig-config libfontconfig1 libunistring0 libgettextpo0 x11-common libice6 libjasper1 liblcms2-2 libpoppler19 libsm6 libxt6 libxmu6 libxpm4 libxaw7 file mime-support bsdmainutils ed gettext-base groff-base man-db html2text gettext intltool-debian po-debconf dh-apparmor debhelper libijs-0.35 libjbig2dec0 libpaper1 gs-cjk-resource libgs9-common libgs9 gsfonts ghostscript libnetpbm10 netpbm tex-common texlive-common texlive-doc-base luatex libgraphite3 libkpathsea6 libptexenc1 texlive-binaries libpaper-utils texlive-base ocaml-base-nox hevea libtinfo-dev libncurses5-dev ocaml-interp ocaml-nox ocaml-compiler-libs preview-latex-style texlive-latex-base ttf-marvosym texlive-fonts-recommended texlive-latex-recommended texlive texlive-humanities texlive-lang-french texlive-pictures texlive-latex-extra texlive-math-extra camlp5 Authentication warning overridden. Get:1 http://ftpmaster.internal/ubuntu/ quantal/main libexpat1 i386 2.0.1-7.2ubuntu1 [130 kB] Get:2 http://ftpmaster.internal/ubuntu/ quantal/main libmagic1 i386 5.11-1 [219 kB] Get:3 http://ftpmaster.internal/ubuntu/ quantal/main libpipeline1 i386 1.2.1-1 [26.1 kB] Get:4 http://ftpmaster.internal/ubuntu/ quantal/main libxau6 i386 1:1.0.7-1 [8582 B] Get:5 http://ftpmaster.internal/ubuntu/ quantal/main libxdmcp6 i386 1:1.1.1-1 [13.1 kB] Get:6 http://ftpmaster.internal/ubuntu/ quantal/main libxcb1 i386 1.8.1-1 [48.5 kB] Get:7 http://ftpmaster.internal/ubuntu/ quantal/main libx11-data all 2:1.4.99.1-0ubuntu2 [168 kB] Get:8 http://ftpmaster.internal/ubuntu/ quantal/main libx11-6 i386 2:1.4.99.1-0ubuntu2 [770 kB] Get:9 http://ftpmaster.internal/ubuntu/ quantal/main libxext6 i386 2:1.3.1-2 [33.9 kB] Get:10 http://ftpmaster.internal/ubuntu/ quantal/main libxml2 i386 2.7.8.dfsg-5.1ubuntu4 [662 kB] Get:11 http://ftpmaster.internal/ubuntu/ quantal/main libavahi-common-data i386 0.6.30-5ubuntu2 [22.2 kB] Get:12 http://ftpmaster.internal/ubuntu/ quantal/main libavahi-common3 i386 0.6.30-5ubuntu2 [26.0 kB] Get:13 http://ftpmaster.internal/ubuntu/ quantal/main libavahi-client3 i386 0.6.30-5ubuntu2 [30.0 kB] Get:14 http://ftpmaster.internal/ubuntu/ quantal/main libcroco3 i386 0.6.5-1 [99.7 kB] Get:15 http://ftpmaster.internal/ubuntu/ quantal/main libcups2 i386 1.5.2-9ubuntu1 [172 kB] Get:16 http://ftpmaster.internal/ubuntu/ quantal/main libjpeg-turbo8 i386 1.1.90+svn733-0ubuntu4 [117 kB] Get:17 http://ftpmaster.internal/ubuntu/ quantal/main libjpeg8 i386 8c-2ubuntu7 [2112 B] Get:18 http://ftpmaster.internal/ubuntu/ quantal/main libtiff4 i386 3.9.5-2ubuntu1 [142 kB] Get:19 http://ftpmaster.internal/ubuntu/ quantal/main libcupsimage2 i386 1.5.2-9ubuntu1 [52.5 kB] Get:20 http://ftpmaster.internal/ubuntu/ quantal/main libfreetype6 i386 2.4.8-1ubuntu2 [345 kB] Get:21 http://ftpmaster.internal/ubuntu/ quantal/main ucf all 3.0025+nmu2ubuntu1 [54.4 kB] Get:22 http://ftpmaster.internal/ubuntu/ quantal/main ttf-dejavu-core all 2.33-2ubuntu1 [1552 kB] Get:23 http://ftpmaster.internal/ubuntu/ quantal/main fontconfig-config all 2.8.0-3ubuntu9 [44.4 kB] Get:24 http://ftpmaster.internal/ubuntu/ quantal/main libfontconfig1 i386 2.8.0-3ubuntu9 [125 kB] Get:25 http://ftpmaster.internal/ubuntu/ quantal/main libunistring0 i386 0.9.3-5 [432 kB] Get:26 http://ftpmaster.internal/ubuntu/ quantal/main libgettextpo0 i386 0.18.1.1-5ubuntu3 [118 kB] Get:27 http://ftpmaster.internal/ubuntu/ quantal/main x11-common all 1:7.6+12ubuntu1 [57.7 kB] Get:28 http://ftpmaster.internal/ubuntu/ quantal/main libice6 i386 2:1.0.8-2 [45.9 kB] Get:29 http://ftpmaster.internal/ubuntu/ quantal/main libjasper1 i386 1.900.1-13 [153 kB] Get:30 http://ftpmaster.internal/ubuntu/ quantal/main liblcms2-2 i386 2.2+git20110628-2ubuntu3 [144 kB] Get:31 http://ftpmaster.internal/ubuntu/ quantal/main libpoppler19 i386 0.18.4-1ubuntu2 [753 kB] Get:32 http://ftpmaster.internal/ubuntu/ quantal/main libsm6 i386 2:1.2.1-2 [17.3 kB] Get:33 http://ftpmaster.internal/ubuntu/ quantal/main libxt6 i386 1:1.1.1-2build1 [180 kB] Get:34 http://ftpmaster.internal/ubuntu/ quantal/main libxmu6 i386 2:1.1.0-3 [52.4 kB] Get:35 http://ftpmaster.internal/ubuntu/ quantal/main libxpm4 i386 1:3.5.9-4 [37.4 kB] Get:36 http://ftpmaster.internal/ubuntu/ quantal/main libxaw7 i386 2:1.0.10-2 [202 kB] Get:37 http://ftpmaster.internal/ubuntu/ quantal/main file i386 5.11-1 [19.6 kB] Get:38 http://ftpmaster.internal/ubuntu/ quantal/main mime-support all 3.51-1ubuntu1 [30.7 kB] Get:39 http://ftpmaster.internal/ubuntu/ quantal/main bsdmainutils i386 8.2.3ubuntu1 [194 kB] Get:40 http://ftpmaster.internal/ubuntu/ quantal/main ed i386 1.6-1 [49.5 kB] Get:41 http://ftpmaster.internal/ubuntu/ quantal/main gettext-base i386 0.18.1.1-5ubuntu3 [58.2 kB] Get:42 http://ftpmaster.internal/ubuntu/ quantal/main groff-base i386 1.21-7 [1024 kB] Get:43 http://ftpmaster.internal/ubuntu/ quantal/main man-db i386 2.6.1-2 [747 kB] Get:44 http://ftpmaster.internal/ubuntu/ quantal/main html2text i386 1.3.2a-15 [101 kB] Get:45 http://ftpmaster.internal/ubuntu/ quantal/main gettext i386 0.18.1.1-5ubuntu3 [1122 kB] Get:46 http://ftpmaster.internal/ubuntu/ quantal/main intltool-debian all 0.35.0+20060710.1 [31.6 kB] Get:47 http://ftpmaster.internal/ubuntu/ quantal/main po-debconf all 1.0.16+nmu2ubuntu1 [210 kB] Get:48 http://ftpmaster.internal/ubuntu/ quantal/main dh-apparmor all 2.7.102-0ubuntu3 [9622 B] Get:49 http://ftpmaster.internal/ubuntu/ quantal/main debhelper all 9.20120419ubuntu2 [609 kB] Get:50 http://ftpmaster.internal/ubuntu/ quantal/main libijs-0.35 i386 0.35-8 [17.0 kB] Get:51 http://ftpmaster.internal/ubuntu/ quantal/main libjbig2dec0 i386 0.11-1ubuntu1 [38.2 kB] Get:52 http://ftpmaster.internal/ubuntu/ quantal/main libpaper1 i386 1.1.24+nmu1build1 [14.0 kB] Get:53 http://ftpmaster.internal/ubuntu/ quantal/main gs-cjk-resource all 1.20100103-3 [1477 kB] Get:54 http://ftpmaster.internal/ubuntu/ quantal/main libgs9-common all 9.05~dfsg-0ubuntu4 [3944 kB] Get:55 http://ftpmaster.internal/ubuntu/ quantal/main libgs9 i386 9.05~dfsg-0ubuntu4 [2258 kB] Get:56 http://ftpmaster.internal/ubuntu/ quantal/main gsfonts all 1:8.11+urwcyr1.0.7~pre44-4.2ubuntu1 [3374 kB] Get:57 http://ftpmaster.internal/ubuntu/ quantal/main ghostscript i386 9.05~dfsg-0ubuntu4 [44.1 kB] Get:58 http://ftpmaster.internal/ubuntu/ quantal/main libnetpbm10 i386 2:10.0-15 [65.3 kB] Get:59 http://ftpmaster.internal/ubuntu/ quantal/main netpbm i386 2:10.0-15 [1176 kB] Get:60 http://ftpmaster.internal/ubuntu/ quantal/main tex-common all 3.10 [626 kB] Get:61 http://ftpmaster.internal/ubuntu/ quantal/main texlive-common all 2011.20120424-1 [219 kB] Get:62 http://ftpmaster.internal/ubuntu/ quantal/main texlive-doc-base all 2011.20120424-1 [1725 kB] Get:63 http://ftpmaster.internal/ubuntu/ quantal/main luatex i386 0.70.1-1ubuntu1 [2366 kB] Get:64 http://ftpmaster.internal/ubuntu/ quantal/main libgraphite3 i386 1:2.3.1-0.2build1 [185 kB] Get:65 http://ftpmaster.internal/ubuntu/ quantal/main libkpathsea6 i386 2011.20120410-1ubuntu1 [72.9 kB] Get:66 http://ftpmaster.internal/ubuntu/ quantal/main libptexenc1 i386 2011.20120410-1ubuntu1 [38.4 kB] Get:67 http://ftpmaster.internal/ubuntu/ quantal/main texlive-binaries i386 2011.20120410-1ubuntu1 [16.6 MB] Get:68 http://ftpmaster.internal/ubuntu/ quantal/main libpaper-utils i386 1.1.24+nmu1build1 [8864 B] Get:69 http://ftpmaster.internal/ubuntu/ quantal/main texlive-base all 2011.20120424-1 [18.6 MB] Get:70 http://ftpmaster.internal/ubuntu/ quantal/main ocaml-base-nox i386 3.12.1-2ubuntu3 [583 kB] Get:71 http://ftpmaster.internal/ubuntu/ quantal/main hevea all 1.10-14build1 [384 kB] Get:72 http://ftpmaster.internal/ubuntu/ quantal/main libtinfo-dev i386 5.9-6 [93.3 kB] Get:73 http://ftpmaster.internal/ubuntu/ quantal/main libncurses5-dev i386 5.9-6 [213 kB] Get:74 http://ftpmaster.internal/ubuntu/ quantal/main ocaml-interp i386 3.12.1-2ubuntu3 [256 kB] Get:75 http://ftpmaster.internal/ubuntu/ quantal/main ocaml-nox i386 3.12.1-2ubuntu3 [7443 kB] Get:76 http://ftpmaster.internal/ubuntu/ quantal/main ocaml-compiler-libs i386 3.12.1-2ubuntu3 [1136 kB] Get:77 http://ftpmaster.internal/ubuntu/ quantal/main preview-latex-style all 11.86-2ubuntu1 [108 kB] Get:78 http://ftpmaster.internal/ubuntu/ quantal/main texlive-latex-base all 2011.20120424-1 [1412 kB] Get:79 http://ftpmaster.internal/ubuntu/ quantal/main ttf-marvosym all 0.1+dfsg-2 [46.9 kB] Get:80 http://ftpmaster.internal/ubuntu/ quantal/main texlive-fonts-recommended all 2011.20120424-1 [7096 kB] Get:81 http://ftpmaster.internal/ubuntu/ quantal/main texlive-latex-recommended all 2011.20120424-1 [7557 kB] Get:82 http://ftpmaster.internal/ubuntu/ quantal/main texlive all 2011.20120424-1 [15.4 kB] Get:83 http://ftpmaster.internal/ubuntu/ quantal/universe texlive-humanities all 2011.20120424-1ubuntu1 [376 kB] Get:84 http://ftpmaster.internal/ubuntu/ quantal/main texlive-lang-french all 2011.20120424-1 [3819 kB] Get:85 http://ftpmaster.internal/ubuntu/ quantal/main texlive-pictures all 2011.20120424-1 [2719 kB] Get:86 http://ftpmaster.internal/ubuntu/ quantal/main texlive-latex-extra all 2011.20120424-1ubuntu1 [7003 kB] Get:87 http://ftpmaster.internal/ubuntu/ quantal/main texlive-math-extra all 2011.20120424-1ubuntu1 [12.7 MB] Get:88 http://ftpmaster.internal/ubuntu/ quantal/main camlp5 i386 6.05-1 [4070 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 121 MB in 9s (13.2 MB/s) Selecting previously unselected package libexpat1. (Reading database ... 12305 files and directories currently installed.) Unpacking libexpat1 (from .../libexpat1_2.0.1-7.2ubuntu1_i386.deb) ... Selecting previously unselected package libmagic1. Unpacking libmagic1 (from .../libmagic1_5.11-1_i386.deb) ... Selecting previously unselected package libpipeline1. Unpacking libpipeline1 (from .../libpipeline1_1.2.1-1_i386.deb) ... Selecting previously unselected package libxau6. Unpacking libxau6 (from .../libxau6_1%3a1.0.7-1_i386.deb) ... Selecting previously unselected package libxdmcp6. Unpacking libxdmcp6 (from .../libxdmcp6_1%3a1.1.1-1_i386.deb) ... Selecting previously unselected package libxcb1. Unpacking libxcb1 (from .../libxcb1_1.8.1-1_i386.deb) ... Selecting previously unselected package libx11-data. Unpacking libx11-data (from .../libx11-data_2%3a1.4.99.1-0ubuntu2_all.deb) ... Selecting previously unselected package libx11-6. Unpacking libx11-6 (from .../libx11-6_2%3a1.4.99.1-0ubuntu2_i386.deb) ... Selecting previously unselected package libxext6. Unpacking libxext6 (from .../libxext6_2%3a1.3.1-2_i386.deb) ... Selecting previously unselected package libxml2. Unpacking libxml2 (from .../libxml2_2.7.8.dfsg-5.1ubuntu4_i386.deb) ... Selecting previously unselected package libavahi-common-data. Unpacking libavahi-common-data (from .../libavahi-common-data_0.6.30-5ubuntu2_i386.deb) ... Selecting previously unselected package libavahi-common3. Unpacking libavahi-common3 (from .../libavahi-common3_0.6.30-5ubuntu2_i386.deb) ... Selecting previously unselected package libavahi-client3. Unpacking libavahi-client3 (from .../libavahi-client3_0.6.30-5ubuntu2_i386.deb) ... Selecting previously unselected package libcroco3. Unpacking libcroco3 (from .../libcroco3_0.6.5-1_i386.deb) ... Selecting previously unselected package libcups2. Unpacking libcups2 (from .../libcups2_1.5.2-9ubuntu1_i386.deb) ... Selecting previously unselected package libjpeg-turbo8. Unpacking libjpeg-turbo8 (from .../libjpeg-turbo8_1.1.90+svn733-0ubuntu4_i386.deb) ... Selecting previously unselected package libjpeg8. Unpacking libjpeg8 (from .../libjpeg8_8c-2ubuntu7_i386.deb) ... Selecting previously unselected package libtiff4. Unpacking libtiff4 (from .../libtiff4_3.9.5-2ubuntu1_i386.deb) ... Selecting previously unselected package libcupsimage2. Unpacking libcupsimage2 (from .../libcupsimage2_1.5.2-9ubuntu1_i386.deb) ... Selecting previously unselected package libfreetype6. Unpacking libfreetype6 (from .../libfreetype6_2.4.8-1ubuntu2_i386.deb) ... Selecting previously unselected package ucf. Unpacking ucf (from .../ucf_3.0025+nmu2ubuntu1_all.deb) ... Moving old data out of the way Selecting previously unselected package ttf-dejavu-core. Unpacking ttf-dejavu-core (from .../ttf-dejavu-core_2.33-2ubuntu1_all.deb) ... Selecting previously unselected package fontconfig-config. Unpacking fontconfig-config (from .../fontconfig-config_2.8.0-3ubuntu9_all.deb) ... Selecting previously unselected package libfontconfig1. Unpacking libfontconfig1 (from .../libfontconfig1_2.8.0-3ubuntu9_i386.deb) ... Selecting previously unselected package libunistring0. Unpacking libunistring0 (from .../libunistring0_0.9.3-5_i386.deb) ... Selecting previously unselected package libgettextpo0. Unpacking libgettextpo0 (from .../libgettextpo0_0.18.1.1-5ubuntu3_i386.deb) ... Selecting previously unselected package x11-common. Unpacking x11-common (from .../x11-common_1%3a7.6+12ubuntu1_all.deb) ... Selecting previously unselected package libice6. Unpacking libice6 (from .../libice6_2%3a1.0.8-2_i386.deb) ... Selecting previously unselected package libjasper1. Unpacking libjasper1 (from .../libjasper1_1.900.1-13_i386.deb) ... Selecting previously unselected package liblcms2-2. Unpacking liblcms2-2 (from .../liblcms2-2_2.2+git20110628-2ubuntu3_i386.deb) ... Selecting previously unselected package libpoppler19. Unpacking libpoppler19 (from .../libpoppler19_0.18.4-1ubuntu2_i386.deb) ... Selecting previously unselected package libsm6. Unpacking libsm6 (from .../libsm6_2%3a1.2.1-2_i386.deb) ... Selecting previously unselected package libxt6. Unpacking libxt6 (from .../libxt6_1%3a1.1.1-2build1_i386.deb) ... Selecting previously unselected package libxmu6. Unpacking libxmu6 (from .../libxmu6_2%3a1.1.0-3_i386.deb) ... Selecting previously unselected package libxpm4. Unpacking libxpm4 (from .../libxpm4_1%3a3.5.9-4_i386.deb) ... Selecting previously unselected package libxaw7. Unpacking libxaw7 (from .../libxaw7_2%3a1.0.10-2_i386.deb) ... Selecting previously unselected package file. Unpacking file (from .../archives/file_5.11-1_i386.deb) ... Selecting previously unselected package mime-support. Unpacking mime-support (from .../mime-support_3.51-1ubuntu1_all.deb) ... Selecting previously unselected package bsdmainutils. Unpacking bsdmainutils (from .../bsdmainutils_8.2.3ubuntu1_i386.deb) ... Selecting previously unselected package ed. Unpacking ed (from .../apt/archives/ed_1.6-1_i386.deb) ... Selecting previously unselected package gettext-base. Unpacking gettext-base (from .../gettext-base_0.18.1.1-5ubuntu3_i386.deb) ... Selecting previously unselected package groff-base. Unpacking groff-base (from .../groff-base_1.21-7_i386.deb) ... Selecting previously unselected package man-db. Unpacking man-db (from .../man-db_2.6.1-2_i386.deb) ... Selecting previously unselected package html2text. Unpacking html2text (from .../html2text_1.3.2a-15_i386.deb) ... Selecting previously unselected package gettext. Unpacking gettext (from .../gettext_0.18.1.1-5ubuntu3_i386.deb) ... Selecting previously unselected package intltool-debian. Unpacking intltool-debian (from .../intltool-debian_0.35.0+20060710.1_all.deb) ... Selecting previously unselected package po-debconf. Unpacking po-debconf (from .../po-debconf_1.0.16+nmu2ubuntu1_all.deb) ... Selecting previously unselected package dh-apparmor. Unpacking dh-apparmor (from .../dh-apparmor_2.7.102-0ubuntu3_all.deb) ... Selecting previously unselected package debhelper. Unpacking debhelper (from .../debhelper_9.20120419ubuntu2_all.deb) ... Selecting previously unselected package libijs-0.35. Unpacking libijs-0.35 (from .../libijs-0.35_0.35-8_i386.deb) ... Selecting previously unselected package libjbig2dec0. Unpacking libjbig2dec0 (from .../libjbig2dec0_0.11-1ubuntu1_i386.deb) ... Selecting previously unselected package libpaper1. Unpacking libpaper1 (from .../libpaper1_1.1.24+nmu1build1_i386.deb) ... Selecting previously unselected package gs-cjk-resource. Unpacking gs-cjk-resource (from .../gs-cjk-resource_1.20100103-3_all.deb) ... Selecting previously unselected package libgs9-common. Unpacking libgs9-common (from .../libgs9-common_9.05~dfsg-0ubuntu4_all.deb) ... Selecting previously unselected package libgs9. Unpacking libgs9 (from .../libgs9_9.05~dfsg-0ubuntu4_i386.deb) ... Selecting previously unselected package gsfonts. Unpacking gsfonts (from .../gsfonts_1%3a8.11+urwcyr1.0.7~pre44-4.2ubuntu1_all.deb) ... Selecting previously unselected package ghostscript. Unpacking ghostscript (from .../ghostscript_9.05~dfsg-0ubuntu4_i386.deb) ... Selecting previously unselected package libnetpbm10. Unpacking libnetpbm10 (from .../libnetpbm10_2%3a10.0-15_i386.deb) ... Selecting previously unselected package netpbm. Unpacking netpbm (from .../netpbm_2%3a10.0-15_i386.deb) ... Selecting previously unselected package tex-common. Unpacking tex-common (from .../tex-common_3.10_all.deb) ... Selecting previously unselected package texlive-common. Unpacking texlive-common (from .../texlive-common_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive-doc-base. Unpacking texlive-doc-base (from .../texlive-doc-base_2011.20120424-1_all.deb) ... Selecting previously unselected package luatex. Unpacking luatex (from .../luatex_0.70.1-1ubuntu1_i386.deb) ... Selecting previously unselected package libgraphite3. Unpacking libgraphite3 (from .../libgraphite3_1%3a2.3.1-0.2build1_i386.deb) ... Selecting previously unselected package libkpathsea6. Unpacking libkpathsea6 (from .../libkpathsea6_2011.20120410-1ubuntu1_i386.deb) ... Selecting previously unselected package libptexenc1. Unpacking libptexenc1 (from .../libptexenc1_2011.20120410-1ubuntu1_i386.deb) ... Selecting previously unselected package texlive-binaries. Unpacking texlive-binaries (from .../texlive-binaries_2011.20120410-1ubuntu1_i386.deb) ... Selecting previously unselected package libpaper-utils. Unpacking libpaper-utils (from .../libpaper-utils_1.1.24+nmu1build1_i386.deb) ... Selecting previously unselected package texlive-base. Unpacking texlive-base (from .../texlive-base_2011.20120424-1_all.deb) ... Selecting previously unselected package ocaml-base-nox. Unpacking ocaml-base-nox (from .../ocaml-base-nox_3.12.1-2ubuntu3_i386.deb) ... Selecting previously unselected package hevea. Unpacking hevea (from .../hevea_1.10-14build1_all.deb) ... Selecting previously unselected package libtinfo-dev. Unpacking libtinfo-dev (from .../libtinfo-dev_5.9-6_i386.deb) ... Selecting previously unselected package libncurses5-dev. Unpacking libncurses5-dev (from .../libncurses5-dev_5.9-6_i386.deb) ... Selecting previously unselected package ocaml-interp. Unpacking ocaml-interp (from .../ocaml-interp_3.12.1-2ubuntu3_i386.deb) ... Selecting previously unselected package ocaml-nox. Unpacking ocaml-nox (from .../ocaml-nox_3.12.1-2ubuntu3_i386.deb) ... Selecting previously unselected package ocaml-compiler-libs. Unpacking ocaml-compiler-libs (from .../ocaml-compiler-libs_3.12.1-2ubuntu3_i386.deb) ... Selecting previously unselected package preview-latex-style. Unpacking preview-latex-style (from .../preview-latex-style_11.86-2ubuntu1_all.deb) ... Selecting previously unselected package texlive-latex-base. Unpacking texlive-latex-base (from .../texlive-latex-base_2011.20120424-1_all.deb) ... Selecting previously unselected package ttf-marvosym. Unpacking ttf-marvosym (from .../ttf-marvosym_0.1+dfsg-2_all.deb) ... Selecting previously unselected package texlive-fonts-recommended. Unpacking texlive-fonts-recommended (from .../texlive-fonts-recommended_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive-latex-recommended. Unpacking texlive-latex-recommended (from .../texlive-latex-recommended_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive. Unpacking texlive (from .../texlive_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive-humanities. Unpacking texlive-humanities (from .../texlive-humanities_2011.20120424-1ubuntu1_all.deb) ... Selecting previously unselected package texlive-lang-french. Unpacking texlive-lang-french (from .../texlive-lang-french_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive-pictures. Unpacking texlive-pictures (from .../texlive-pictures_2011.20120424-1_all.deb) ... Selecting previously unselected package texlive-latex-extra. Unpacking texlive-latex-extra (from .../texlive-latex-extra_2011.20120424-1ubuntu1_all.deb) ... Selecting previously unselected package texlive-math-extra. Unpacking texlive-math-extra (from .../texlive-math-extra_2011.20120424-1ubuntu1_all.deb) ... Selecting previously unselected package camlp5. Unpacking camlp5 (from .../camlp5_6.05-1_i386.deb) ... Setting up libexpat1 (2.0.1-7.2ubuntu1) ... Setting up libmagic1 (5.11-1) ... Setting up libpipeline1 (1.2.1-1) ... Setting up libxau6 (1:1.0.7-1) ... Setting up libxdmcp6 (1:1.1.1-1) ... Setting up libxcb1 (1.8.1-1) ... Setting up libx11-data (2:1.4.99.1-0ubuntu2) ... Setting up libx11-6 (2:1.4.99.1-0ubuntu2) ... Setting up libxext6 (2:1.3.1-2) ... Setting up libxml2 (2.7.8.dfsg-5.1ubuntu4) ... Setting up libavahi-common-data (0.6.30-5ubuntu2) ... Setting up libavahi-common3 (0.6.30-5ubuntu2) ... Setting up libavahi-client3 (0.6.30-5ubuntu2) ... Setting up libcroco3 (0.6.5-1) ... Setting up libcups2 (1.5.2-9ubuntu1) ... Setting up libjpeg-turbo8 (1.1.90+svn733-0ubuntu4) ... Setting up libjpeg8 (8c-2ubuntu7) ... Setting up libtiff4 (3.9.5-2ubuntu1) ... Setting up libcupsimage2 (1.5.2-9ubuntu1) ... Setting up libfreetype6 (2.4.8-1ubuntu2) ... Setting up ucf (3.0025+nmu2ubuntu1) ... Setting up ttf-dejavu-core (2.33-2ubuntu1) ... Setting up fontconfig-config (2.8.0-3ubuntu9) ... Setting up libfontconfig1 (2.8.0-3ubuntu9) ... Setting up libunistring0 (0.9.3-5) ... Setting up libgettextpo0 (0.18.1.1-5ubuntu3) ... Setting up x11-common (1:7.6+12ubuntu1) ... invoke-rc.d: policy-rc.d denied execution of start. Setting up libice6 (2:1.0.8-2) ... Setting up libjasper1 (1.900.1-13) ... Setting up liblcms2-2 (2.2+git20110628-2ubuntu3) ... Setting up libpoppler19 (0.18.4-1ubuntu2) ... Setting up libsm6 (2:1.2.1-2) ... Setting up libxt6 (1:1.1.1-2build1) ... Setting up libxmu6 (2:1.1.0-3) ... Setting up libxpm4 (1:3.5.9-4) ... Setting up libxaw7 (2:1.0.10-2) ... Setting up file (5.11-1) ... Setting up mime-support (3.51-1ubuntu1) ... update-alternatives: using /usr/bin/see to provide /usr/bin/view (view) in auto mode. Setting up bsdmainutils (8.2.3ubuntu1) ... update-alternatives: using /usr/bin/bsd-write to provide /usr/bin/write (write) in auto mode. update-alternatives: using /usr/bin/bsd-from to provide /usr/bin/from (from) in auto mode. Setting up ed (1.6-1) ... Setting up gettext-base (0.18.1.1-5ubuntu3) ... Setting up groff-base (1.21-7) ... Setting up man-db (2.6.1-2) ... Building database of manual pages ... Setting up html2text (1.3.2a-15) ... Setting up gettext (0.18.1.1-5ubuntu3) ... Setting up intltool-debian (0.35.0+20060710.1) ... Setting up po-debconf (1.0.16+nmu2ubuntu1) ... Setting up dh-apparmor (2.7.102-0ubuntu3) ... Setting up debhelper (9.20120419ubuntu2) ... Setting up libijs-0.35 (0.35-8) ... Setting up libjbig2dec0 (0.11-1ubuntu1) ... Setting up libpaper1 (1.1.24+nmu1build1) ... Creating config file /etc/papersize with new version Setting up libgs9-common (9.05~dfsg-0ubuntu4) ... update-alternatives: using /usr/share/ghostscript/9.05 to provide /usr/share/ghostscript/current (ghostscript-current) in auto mode. Setting up gsfonts (1:8.11+urwcyr1.0.7~pre44-4.2ubuntu1) ... Setting up libnetpbm10 (2:10.0-15) ... Setting up netpbm (2:10.0-15) ... Setting up tex-common (3.10) ... Running mktexlsr. This may take some time... done. texlive-base is not ready, delaying updmap-sys call texlive-base is not ready, skipping fmtutil-sys --all call Setting up texlive-common (2011.20120424-1) ... Setting up texlive-doc-base (2011.20120424-1) ... Setting up luatex (0.70.1-1ubuntu1) ... texlive-base is not ready, cannot create formats Setting up libgraphite3 (1:2.3.1-0.2build1) ... Setting up libkpathsea6 (2011.20120410-1ubuntu1) ... Setting up libptexenc1 (2011.20120410-1ubuntu1) ... Setting up texlive-binaries (2011.20120410-1ubuntu1) ... update-alternatives: using /usr/bin/xdvi-xaw to provide /usr/bin/xdvi.bin (xdvi.bin) in auto mode. update-alternatives: using /usr/bin/bibtex.original to provide /usr/bin/bibtex (bibtex) in auto mode. Building format(s) --refresh. This may take some time... done. Setting up libpaper-utils (1.1.24+nmu1build1) ... Setting up ocaml-base-nox (3.12.1-2ubuntu3) ... Setting up libtinfo-dev (5.9-6) ... Setting up libncurses5-dev (5.9-6) ... Setting up ocaml-interp (3.12.1-2ubuntu3) ... Setting up ocaml-nox (3.12.1-2ubuntu3) ... Setting up ocaml-compiler-libs (3.12.1-2ubuntu3) ... Setting up preview-latex-style (11.86-2ubuntu1) ... Setting up ttf-marvosym (0.1+dfsg-2) ... Setting up camlp5 (6.05-1) ... Processing triggers for tex-common ... Running mktexlsr. This may take some time... done. Setting up texlive-base (2011.20120424-1) ... /usr/bin/tl-paper: setting paper size for dvips to a4. /usr/bin/tl-paper: setting paper size for dvipdfmx to a4. /usr/bin/tl-paper: setting paper size for xdvi to a4. /usr/bin/tl-paper: setting paper size for pdftex to a4. Running mktexlsr. This may take some time... done. Building format(s) --all. This may take some time... done. Processing triggers for tex-common ... Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Setting up texlive-fonts-recommended (2011.20120424-1) ... Setting up texlive-lang-french (2011.20120424-1) ... Setting up texlive-pictures (2011.20120424-1) ... Setting up texlive-latex-base (2011.20120424-1) ... Running mktexlsr. This may take some time... done. Building format(s) --all --cnffile /etc/texmf/fmt.d/10texlive-latex-base.cnf. This may take some time... done. Processing triggers for tex-common ... Running mktexlsr. This may take some time... done. Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Building latex-based formats --byhyphen /var/lib/texmf/tex/generic/config/language.dat. This may take some time... done. Building e-tex based formats --byhyphen /var/lib/texmf/tex/generic/config/language.def. This may take some time... done. Setting up texlive-humanities (2011.20120424-1ubuntu1) ... Setting up texlive-math-extra (2011.20120424-1ubuntu1) ... Running mktexlsr. This may take some time... done. Building format(s) --all --cnffile /etc/texmf/fmt.d/10texlive-math-extra.cnf. This may take some time... done. Setting up texlive-latex-recommended (2011.20120424-1) ... Processing triggers for tex-common ... Running mktexlsr. This may take some time... done. Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Setting up texlive (2011.20120424-1) ... Setting up texlive-latex-extra (2011.20120424-1ubuntu1) ... Processing triggers for tex-common ... Running mktexlsr. This may take some time... done. Running updmap-sys. This may take some time... done. Running mktexlsr /var/lib/texmf ... done. Setting up gs-cjk-resource (1.20100103-3) ... Setting up libgs9 (9.05~dfsg-0ubuntu4) ... Setting up ghostscript (9.05~dfsg-0ubuntu4) ... Setting up hevea (1.10-14build1) ... Processing triggers for libc-bin ... ldconfig deferred processing now taking place Processing triggers for tex-common ... Running mktexlsr. This may take some time... done. Checking correctness of source dependencies... Toolchain package versions: libc6-dev_2.15-0ubuntu10 make_3.81-8.1ubuntu1 dpkg-dev_1.16.1.2ubuntu8 gcc-4.7_4.7.0-7ubuntu1 g++-4.7_4.7.0-7ubuntu1 binutils_2.22-6ubuntu1 libstdc++6-4.7-dev_4.7.0-7ubuntu1 libstdc++6_4.7.0-7ubuntu1 ------------------------------------------------------------------------------ dpkg-source: warning: -sn is not a valid option for Dpkg::Source::Package::V3::quilt gpgv: Signature made Fri Apr 6 06:06:06 2012 UTC using RSA key ID 49881AD3 gpgv: Can't check signature: public key not found dpkg-source: warning: failed to verify signature on ./coq-doc_8.3pl4-1.dsc dpkg-source: info: extracting coq-doc in coq-doc-8.3pl4 dpkg-source: info: unpacking coq-doc_8.3pl4.orig.tar.gz dpkg-source: info: unpacking coq-doc_8.3pl4-1.debian.tar.gz dpkg-buildpackage: source package coq-doc dpkg-buildpackage: source version 8.3pl4-1 dpkg-source --before-build coq-doc-8.3pl4 dpkg-buildpackage: host architecture i386 /usr/bin/fakeroot debian/rules clean dh clean dh_testdir dh_auto_clean make[1]: Entering directory `/build/buildd/coq-doc-8.3pl4' rm -f bin/coqide.byte bin/coqide.opt bin/coqide rm -f ide/input_method_lexer.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 states/*.coq find theories -name '*.vo' -o -name '*.glob' | xargs rm -f rm -f bin/coqtop bin/coqmktop bin/coqc bin/coqchk bin/coqdep_boot rm -f bin/coqtop.opt bin/coqmktop.opt bin/coqc.opt bin/coqchk.opt find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f rm -f bin/coqdep bin/coq_makefile bin/gallina bin/coq-tex bin/coqwc bin/coqdoc plugins/micromega/csdpcert rm -rf _build myocamlbuild_config.ml rm -f dev/ocamlweb-doc/lex.ml tools/gallina_lexer.ml tools/coqdoc/cpretty.ml tools/coqwc.ml tools/coqdep_lexer.ml plugins/dp/dp_zenon.ml ide/utf8_convert.ml ide/config_lexer.ml ide/highlight.ml ide/coq_lex.ml dev/ocamlweb-doc/syntax.ml ide/config_parser.ml scripts/tolink.ml kernel/copcodes.ml dev/ocamlweb-doc/syntax.mli ide/config_parser.mli kernel/byterun/coq_jumptbl.h theories/Numbers/Natural/BigN/NMake_gen.v rm -f bin/coqtop.byte bin/coqmktop.byte bin/coqc.byte bin/coqchk.byte find . -name '*~' -o -name '*.cm[ioa]' | xargs rm -f find . -name '*_mod.ml' | xargs rm -f find plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f rm -f */*.pp[iox] plugins/*/*.pp[iox] rm -rf dev/source-doc rm -f toplevel/mltop.byteml toplevel/mltop.optml rm -f test-suite/check.log rm -f glob.dump rm -f config/revision.ml revision make -C test-suite clean make[2]: Entering directory `/build/buildd/coq-doc-8.3pl4/test-suite' rm -f trace lia.cache RM <**/*.stamp> <**/*.vo> <**/*.log> make[2]: Leaving directory `/build/buildd/coq-doc-8.3pl4/test-suite' rm -f lib/pp.ml lib/compat.ml lib/refutpat.ml toplevel/whelp.ml toplevel/mltop.ml tools/coq_tex.ml tools/coq_makefile.ml plugins/ring/g_ring.ml plugins/firstorder/g_ground.ml plugins/nsatz/nsatz.ml plugins/funind/g_indfun.ml plugins/setoid_ring/newring.ml plugins/quote/g_quote.ml plugins/fourier/g_fourier.ml plugins/omega/g_omega.ml plugins/subtac/g_subtac.ml plugins/micromega/g_micromega.ml plugins/cc/g_congruence.ml plugins/dp/g_dp.ml plugins/rtauto/g_rtauto.ml plugins/field/field.ml plugins/extraction/g_extraction.ml plugins/xml/xmlentries.ml plugins/xml/proofTree2Xml.ml plugins/xml/xml.ml plugins/xml/acic2Xml.ml plugins/xml/dumptree.ml plugins/romega/g_romega.ml tactics/extratactics.ml tactics/eauto.ml tactics/rewrite.ml tactics/eqdecide.ml tactics/hipattern.ml tactics/extraargs.ml tactics/tauto.ml tactics/class_tactics.ml parsing/vernacextend.ml parsing/g_constr.ml parsing/q_constr.ml parsing/g_xml.ml parsing/g_decl_mode.ml parsing/tacextend.ml parsing/q_util.ml parsing/g_ltac.ml parsing/q_coqast.ml parsing/g_tactic.ml parsing/g_proofs.ml parsing/g_vernac.ml parsing/lexer.ml parsing/argextend.ml parsing/g_prim.ml parsing/pcoq.ml lib/pp.ml4-preprocessed lib/compat.ml4-preprocessed lib/refutpat.ml4-preprocessed toplevel/whelp.ml4-preprocessed toplevel/mltop.ml4-preprocessed tools/coq_tex.ml4-preprocessed tools/coq_makefile.ml4-preprocessed plugins/ring/g_ring.ml4-preprocessed plugins/firstorder/g_ground.ml4-preprocessed plugins/nsatz/nsatz.ml4-preprocessed plugins/funind/g_indfun.ml4-preprocessed plugins/setoid_ring/newring.ml4-preprocessed plugins/quote/g_quote.ml4-preprocessed plugins/fourier/g_fourier.ml4-preprocessed plugins/omega/g_omega.ml4-preprocessed plugins/subtac/g_subtac.ml4-preprocessed plugins/micromega/g_micromega.ml4-preprocessed plugins/cc/g_congruence.ml4-preprocessed plugins/dp/g_dp.ml4-preprocessed plugins/rtauto/g_rtauto.ml4-preprocessed plugins/field/field.ml4-preprocessed plugins/extraction/g_extraction.ml4-preprocessed plugins/xml/xmlentries.ml4-preprocessed plugins/xml/proofTree2Xml.ml4-preprocessed plugins/xml/xml.ml4-preprocessed plugins/xml/acic2Xml.ml4-preprocessed plugins/xml/dumptree.ml4-preprocessed plugins/romega/g_romega.ml4-preprocessed tactics/extratactics.ml4-preprocessed tactics/eauto.ml4-preprocessed tactics/rewrite.ml4-preprocessed tactics/eqdecide.ml4-preprocessed tactics/hipattern.ml4-preprocessed tactics/extraargs.ml4-preprocessed tactics/tauto.ml4-preprocessed tactics/class_tactics.ml4-preprocessed parsing/vernacextend.ml4-preprocessed parsing/g_constr.ml4-preprocessed parsing/q_constr.ml4-preprocessed parsing/g_xml.ml4-preprocessed parsing/g_decl_mode.ml4-preprocessed parsing/tacextend.ml4-preprocessed parsing/q_util.ml4-preprocessed parsing/g_ltac.ml4-preprocessed parsing/q_coqast.ml4-preprocessed parsing/g_tactic.ml4-preprocessed parsing/g_proofs.ml4-preprocessed parsing/g_vernac.ml4-preprocessed parsing/lexer.ml4-preprocessed parsing/argextend.ml4-preprocessed parsing/g_prim.ml4-preprocessed parsing/pcoq.ml4-preprocessed find . -name '*~' -o -name '*.annot' | xargs rm -f rm -f gmon.out core find . '(' -name '{arch}' -o -name '.svn' -o -name '_darcs' -o -name '.git' -o -name '.bzr' -o -name 'debian' -o -name "${GIT_DIR}" -o -name '_build' ')' -prune -o '(' -name '*.d' ')' -print | xargs rm -f rm -f doc/*/*.dvi doc/*/*.aux doc/*/*.log doc/*/*.bbl doc/*/*.blg doc/*/*.toc \ doc/*/*.idx doc/*/*~ doc/*/*.ilg doc/*/*.ind doc/*/*.dvi.gz doc/*/*.ps.gz doc/*/*.pdf.gz\ doc/*/*.???idx doc/*/*.???ind doc/*/*.v.tex doc/*/*.atoc doc/*/*.lof\ doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \ doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \ doc/stdlib/library.files.ls rm -f doc/*/*.ps doc/*/*.pdf rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html rm -f doc/refman/euclid.ml doc/refman/euclid.mli rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli rm -f doc/common/version.tex rm -f doc/refman/styles.hva doc/refman/cover.html doc/refman/Reference-Manual.html rm -f doc/coq.tex rm -f doc/refman/styles.hva doc/refman/cover.html find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \; rm -f config/Makefile config/coq_config.ml dev/ocamldebug-v7 ide/undo.mli make -C test-suite distclean make[2]: Entering directory `/build/buildd/coq-doc-8.3pl4/test-suite' rm -f trace lia.cache RM <**/*.stamp> <**/*.vo> <**/*.log> make[2]: Leaving directory `/build/buildd/coq-doc-8.3pl4/test-suite' make[1]: Leaving directory `/build/buildd/coq-doc-8.3pl4' dh_clean debian/rules build make: `build' is up to date. /usr/bin/fakeroot debian/rules binary dh binary dh_testdir debian/rules override_dh_auto_configure make[1]: Entering directory `/build/buildd/coq-doc-8.3pl4' ./configure -local You have GNU Make 3.81. Good! You have Objective-Caml 3.12.1. Good! You have native-code compilation. Good! LablGtk2 not found: CoqIde will not be available. Coq top directory : /build/buildd/coq-doc-8.3pl4 Architecture : i686 Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/build/buildd/coq-doc-8.3pl4'/kernel/byterun Coq tools bytecode link flags : OS dependent libraries : -cclib -lunix Objective-Caml/Camlp4 version : 3.12.1 Objective-Caml/Camlp4 binaries in : /usr/bin Objective-Caml library in : /usr/lib/ocaml Camlp4 library in : +camlp5 Native dynamic link support : true Documentation : All CoqIde : no Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s & Coq web site : http://coq.inria.fr/ Paths for true installation: binaries will be copied in /build/buildd/coq-doc-8.3pl4/bin library will be copied in /build/buildd/coq-doc-8.3pl4 man pages will be copied in /build/buildd/coq-doc-8.3pl4/man documentation will be copied in /build/buildd/coq-doc-8.3pl4/doc emacs mode will be copied in /build/buildd/coq-doc-8.3pl4/tools/emacs 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'. make[1]: Leaving directory `/build/buildd/coq-doc-8.3pl4' debian/rules override_dh_auto_build make[1]: Entering directory `/build/buildd/coq-doc-8.3pl4' /usr/bin/make refman faq tutorial rectutorial make[2]: Entering directory `/build/buildd/coq-doc-8.3pl4' ***************************************************** ***************************************************** ****************** Entering stage1 ****************** ***************************************************** ***************************************************** /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage1 "stage1" make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \ -e '/^}/q' kernel/byterun/coq_instruct.h > \ kernel/byterun/coq_jumptbl.h \ || ( RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV} ) CCDEP kernel/byterun/coq_values.c CCDEP kernel/byterun/coq_memory.c CCDEP kernel/byterun/coq_fix_code.c CCDEP kernel/byterun/coq_interp.c OCAMLLEX dev/ocamlweb-doc/lex.mll 99 states, 6415 transitions, table size 26254 bytes OCAMLLEX tools/gallina_lexer.mll 190 states, 498 transitions, table size 3132 bytes OCAMLLEX tools/coqdoc/cpretty.mll 2138 states, 6918 transitions, table size 40500 bytes OCAMLLEX tools/coqwc.mll 230 states, 833 transitions, table size 4712 bytes OCAMLLEX tools/coqdep_lexer.mll 200 states, 5470 transitions, table size 23080 bytes 2243 additional bytes used for bindings OCAMLLEX plugins/dp/dp_zenon.mll 85 states, 637 transitions, table size 3058 bytes 1881 additional bytes used for bindings OCAMLLEX ide/utf8_convert.mll 15 states, 827 transitions, table size 3398 bytes OCAMLLEX ide/config_lexer.mll 13 states, 332 transitions, table size 1406 bytes OCAMLLEX ide/highlight.mll 455 states, 31494 transitions, table size 128706 bytes OCAMLLEX ide/coq_lex.mll 457 states, 31161 transitions, table size 127386 bytes OCAMLYACC dev/ocamlweb-doc/syntax.mly 3 shift/reduce conflicts. OCAMLYACC ide/config_parser.mly ECHO... > scripts/tolink.ml sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' \ kernel/byterun/coq_instruct.h | \ awk -f kernel/make-opcodes > kernel/copcodes.ml \ || ( RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV} ) "ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > theories/Numbers/Natural/BigN/NMake_gen.v TOUCH lib/pp.ml TOUCH lib/compat.ml TOUCH lib/refutpat.ml TOUCH toplevel/whelp.ml TOUCH toplevel/mltop.ml TOUCH tools/coq_tex.ml TOUCH tools/coq_makefile.ml TOUCH plugins/ring/g_ring.ml TOUCH plugins/firstorder/g_ground.ml TOUCH plugins/nsatz/nsatz.ml TOUCH plugins/funind/g_indfun.ml TOUCH plugins/setoid_ring/newring.ml TOUCH plugins/quote/g_quote.ml TOUCH plugins/fourier/g_fourier.ml TOUCH plugins/omega/g_omega.ml TOUCH plugins/subtac/g_subtac.ml TOUCH plugins/micromega/g_micromega.ml TOUCH plugins/cc/g_congruence.ml TOUCH plugins/dp/g_dp.ml TOUCH plugins/rtauto/g_rtauto.ml TOUCH plugins/field/field.ml TOUCH plugins/extraction/g_extraction.ml TOUCH plugins/xml/xmlentries.ml TOUCH plugins/xml/proofTree2Xml.ml TOUCH plugins/xml/xml.ml TOUCH plugins/xml/acic2Xml.ml TOUCH plugins/xml/dumptree.ml TOUCH plugins/romega/g_romega.ml TOUCH tactics/extratactics.ml TOUCH tactics/eauto.ml TOUCH tactics/rewrite.ml TOUCH tactics/eqdecide.ml TOUCH tactics/hipattern.ml TOUCH tactics/extraargs.ml TOUCH tactics/tauto.ml TOUCH tactics/class_tactics.ml TOUCH parsing/vernacextend.ml TOUCH parsing/g_constr.ml TOUCH parsing/q_constr.ml TOUCH parsing/g_xml.ml TOUCH parsing/g_decl_mode.ml TOUCH parsing/tacextend.ml TOUCH parsing/q_util.ml TOUCH parsing/g_ltac.ml TOUCH parsing/q_coqast.ml TOUCH parsing/g_tactic.ml TOUCH parsing/g_proofs.ml TOUCH parsing/g_vernac.ml TOUCH parsing/lexer.ml TOUCH parsing/argextend.ml TOUCH parsing/g_prim.ml TOUCH parsing/pcoq.ml CAMLP4DEPS parsing/q_constr.ml4 OCAMLDEP4 parsing/q_constr.ml4 CAMLP4DEPS parsing/q_coqast.ml4 OCAMLDEP4 parsing/q_coqast.ml4 CAMLP4DEPS parsing/lexer.ml4 OCAMLDEP4 parsing/lexer.ml4 CAMLP4DEPS parsing/g_constr.ml4 OCAMLDEP4 parsing/g_constr.ml4 CAMLP4DEPS parsing/g_ltac.ml4 OCAMLDEP4 parsing/g_ltac.ml4 CAMLP4DEPS parsing/g_tactic.ml4 OCAMLDEP4 parsing/g_tactic.ml4 CAMLP4DEPS parsing/g_prim.ml4 OCAMLDEP4 parsing/g_prim.ml4 CAMLP4DEPS parsing/vernacextend.ml4 OCAMLDEP4 parsing/vernacextend.ml4 CAMLP4DEPS parsing/tacextend.ml4 OCAMLDEP4 parsing/tacextend.ml4 CAMLP4DEPS parsing/argextend.ml4 OCAMLDEP4 parsing/argextend.ml4 CAMLP4DEPS parsing/pcoq.ml4 OCAMLDEP4 parsing/pcoq.ml4 CAMLP4DEPS parsing/q_util.ml4 OCAMLDEP4 parsing/q_util.ml4 CAMLP4DEPS lib/pp.ml4 OCAMLDEP4 lib/pp.ml4 CAMLP4DEPS lib/compat.ml4 OCAMLDEP4 lib/compat.ml4 OCAMLDEP ide/config_parser.mli OCAMLDEP dev/ocamlweb-doc/syntax.mli OCAMLDEP config/coq_config.mli OCAMLDEP proofs/tactic_debug.mli OCAMLDEP proofs/decl_expr.mli OCAMLDEP proofs/pfedit.mli OCAMLDEP proofs/decl_mode.mli OCAMLDEP proofs/evar_refiner.mli OCAMLDEP proofs/refiner.mli OCAMLDEP proofs/redexpr.mli OCAMLDEP proofs/clenvtac.mli OCAMLDEP proofs/logic.mli OCAMLDEP proofs/proof_trees.mli OCAMLDEP proofs/tacmach.mli OCAMLDEP proofs/proof_type.mli OCAMLDEP interp/ppextend.mli OCAMLDEP interp/notation.mli OCAMLDEP interp/syntax_def.mli OCAMLDEP interp/constrextern.mli OCAMLDEP interp/genarg.mli OCAMLDEP interp/coqlib.mli OCAMLDEP interp/implicit_quantifiers.mli OCAMLDEP interp/dumpglob.mli OCAMLDEP interp/modintern.mli OCAMLDEP interp/topconstr.mli OCAMLDEP interp/reserve.mli OCAMLDEP interp/smartlocate.mli OCAMLDEP interp/constrintern.mli OCAMLDEP parsing/g_intsyntax.mli OCAMLDEP parsing/pcoq.mli OCAMLDEP parsing/printmod.mli OCAMLDEP parsing/ppdecl_proof.mli OCAMLDEP parsing/pptactic.mli OCAMLDEP parsing/ppconstr.mli OCAMLDEP parsing/tactic_printer.mli OCAMLDEP parsing/q_util.mli OCAMLDEP parsing/extend.mli OCAMLDEP parsing/ppvernac.mli OCAMLDEP parsing/prettyp.mli OCAMLDEP parsing/extrawit.mli OCAMLDEP parsing/g_zsyntax.mli OCAMLDEP parsing/g_natsyntax.mli OCAMLDEP parsing/egrammar.mli OCAMLDEP parsing/lexer.mli OCAMLDEP parsing/printer.mli OCAMLDEP tactics/tactic_option.mli OCAMLDEP tactics/extratactics.mli OCAMLDEP tactics/refine.mli OCAMLDEP tactics/btermdn.mli OCAMLDEP tactics/eqschemes.mli OCAMLDEP tactics/decl_proof_instr.mli OCAMLDEP tactics/elimschemes.mli OCAMLDEP tactics/tacticals.mli OCAMLDEP tactics/decl_interp.mli OCAMLDEP tactics/auto.mli OCAMLDEP tactics/tacinterp.mli OCAMLDEP tactics/dn.mli OCAMLDEP tactics/autorewrite.mli OCAMLDEP tactics/tactics.mli OCAMLDEP tactics/termdn.mli OCAMLDEP tactics/dhyp.mli OCAMLDEP tactics/nbtermdn.mli OCAMLDEP tactics/extraargs.mli OCAMLDEP tactics/eauto.mli OCAMLDEP tactics/evar_tactics.mli OCAMLDEP tactics/leminv.mli OCAMLDEP tactics/hipattern.mli OCAMLDEP tactics/contradiction.mli OCAMLDEP tactics/equality.mli OCAMLDEP tactics/hiddentac.mli OCAMLDEP tactics/inv.mli OCAMLDEP tactics/elim.mli OCAMLDEP checker/environ.mli OCAMLDEP checker/term.mli OCAMLDEP checker/modops.mli OCAMLDEP checker/inductive.mli OCAMLDEP checker/safe_typing.mli OCAMLDEP checker/reduction.mli OCAMLDEP checker/closure.mli OCAMLDEP checker/declarations.mli OCAMLDEP checker/subtyping.mli OCAMLDEP checker/typeops.mli OCAMLDEP checker/check_stat.mli OCAMLDEP checker/type_errors.mli OCAMLDEP checker/indtypes.mli OCAMLDEP ide/undo_lablgtk_ge212.mli OCAMLDEP ide/coq.mli OCAMLDEP ide/undo_lablgtk_ge26.mli OCAMLDEP ide/coq_tactics.mli OCAMLDEP ide/utils/okey.mli OCAMLDEP ide/utils/config_file.mli OCAMLDEP ide/utils/configwin.mli OCAMLDEP ide/undo_lablgtk_lt26.mli OCAMLDEP ide/command_windows.mli OCAMLDEP ide/preferences.mli OCAMLDEP ide/coqide.mli OCAMLDEP ide/ideutils.mli OCAMLDEP pretyping/term_dnet.mli OCAMLDEP pretyping/clenv.mli OCAMLDEP pretyping/typeclasses_errors.mli OCAMLDEP pretyping/indrec.mli OCAMLDEP pretyping/typing.mli OCAMLDEP pretyping/recordops.mli OCAMLDEP pretyping/classops.mli OCAMLDEP pretyping/unification.mli OCAMLDEP pretyping/cases.mli OCAMLDEP pretyping/namegen.mli OCAMLDEP pretyping/evd.mli OCAMLDEP pretyping/detyping.mli OCAMLDEP pretyping/reductionops.mli OCAMLDEP pretyping/cbv.mli OCAMLDEP pretyping/retyping.mli OCAMLDEP pretyping/pretyping.mli OCAMLDEP pretyping/rawterm.mli OCAMLDEP pretyping/evarconv.mli OCAMLDEP pretyping/vnorm.mli OCAMLDEP pretyping/termops.mli OCAMLDEP pretyping/evarutil.mli OCAMLDEP pretyping/coercion.mli OCAMLDEP pretyping/tacred.mli OCAMLDEP pretyping/typeclasses.mli OCAMLDEP pretyping/pretype_errors.mli OCAMLDEP pretyping/matching.mli OCAMLDEP pretyping/pattern.mli OCAMLDEP pretyping/inductiveops.mli OCAMLDEP plugins/romega/const_omega.mli OCAMLDEP plugins/xml/doubleTypeInference.mli OCAMLDEP plugins/xml/xmlcommand.mli OCAMLDEP plugins/xml/unshare.mli OCAMLDEP plugins/xml/xml.mli OCAMLDEP plugins/extraction/mlutil.mli OCAMLDEP plugins/extraction/table.mli OCAMLDEP plugins/extraction/modutil.mli OCAMLDEP plugins/extraction/haskell.mli OCAMLDEP plugins/extraction/extract_env.mli OCAMLDEP plugins/extraction/scheme.mli OCAMLDEP plugins/extraction/ocaml.mli OCAMLDEP plugins/extraction/extraction.mli OCAMLDEP plugins/extraction/common.mli OCAMLDEP plugins/extraction/miniml.mli OCAMLDEP plugins/rtauto/proof_search.mli OCAMLDEP plugins/rtauto/refl_tauto.mli OCAMLDEP plugins/dp/dp_zenon.mli OCAMLDEP plugins/dp/dp_why.mli OCAMLDEP plugins/dp/fol.mli OCAMLDEP plugins/dp/dp.mli OCAMLDEP plugins/cc/ccproof.mli OCAMLDEP plugins/cc/cctac.mli OCAMLDEP plugins/cc/ccalgo.mli OCAMLDEP plugins/micromega/sos.mli OCAMLDEP plugins/micromega/micromega.mli OCAMLDEP plugins/subtac/subtac_pretyping.mli OCAMLDEP plugins/subtac/subtac_errors.mli OCAMLDEP plugins/subtac/subtac_classes.mli OCAMLDEP plugins/subtac/subtac_utils.mli OCAMLDEP plugins/subtac/subtac_command.mli OCAMLDEP plugins/subtac/subtac.mli OCAMLDEP plugins/subtac/subtac_coercion.mli OCAMLDEP plugins/subtac/subtac_cases.mli OCAMLDEP plugins/subtac/subtac_obligations.mli OCAMLDEP plugins/subtac/eterm.mli OCAMLDEP plugins/funind/rawterm_to_relation.mli OCAMLDEP plugins/funind/indfun_common.mli OCAMLDEP plugins/funind/rawtermops.mli OCAMLDEP plugins/funind/functional_principles_types.mli OCAMLDEP plugins/funind/functional_principles_proofs.mli OCAMLDEP plugins/nsatz/polynom.mli OCAMLDEP plugins/nsatz/utile.mli OCAMLDEP plugins/firstorder/ground.mli OCAMLDEP plugins/firstorder/rules.mli OCAMLDEP plugins/firstorder/sequent.mli OCAMLDEP plugins/firstorder/formula.mli OCAMLDEP plugins/firstorder/unify.mli OCAMLDEP plugins/firstorder/instances.mli OCAMLDEP tools/coqdoc/index.mli OCAMLDEP tools/coqdoc/tokens.mli OCAMLDEP tools/coqdoc/cpretty.mli OCAMLDEP tools/coqdoc/output.mli OCAMLDEP tools/coqdoc/alpha.mli OCAMLDEP toplevel/autoinstance.mli OCAMLDEP toplevel/command.mli OCAMLDEP toplevel/vernacinterp.mli OCAMLDEP toplevel/himsg.mli OCAMLDEP toplevel/mltop.mli OCAMLDEP toplevel/search.mli OCAMLDEP toplevel/lemmas.mli OCAMLDEP toplevel/ind_tables.mli OCAMLDEP toplevel/auto_ind_decl.mli OCAMLDEP toplevel/cerrors.mli OCAMLDEP toplevel/coqinit.mli OCAMLDEP toplevel/vernac.mli OCAMLDEP toplevel/toplevel.mli OCAMLDEP toplevel/class.mli OCAMLDEP toplevel/coqtop.mli OCAMLDEP toplevel/whelp.mli OCAMLDEP toplevel/record.mli OCAMLDEP toplevel/usage.mli OCAMLDEP toplevel/vernacentries.mli OCAMLDEP toplevel/classes.mli OCAMLDEP toplevel/discharge.mli OCAMLDEP toplevel/metasyntax.mli OCAMLDEP toplevel/indschemes.mli OCAMLDEP toplevel/libtypes.mli OCAMLDEP lib/gmap.mli OCAMLDEP lib/gset.mli OCAMLDEP lib/predicate.mli OCAMLDEP lib/bigint.mli OCAMLDEP lib/pp_control.mli OCAMLDEP lib/fmap.mli OCAMLDEP lib/tlm.mli OCAMLDEP lib/dyn.mli OCAMLDEP lib/pp.mli OCAMLDEP lib/rtree.mli OCAMLDEP lib/tries.mli OCAMLDEP lib/fset.mli OCAMLDEP lib/edit.mli OCAMLDEP lib/explore.mli OCAMLDEP lib/heap.mli OCAMLDEP lib/system.mli OCAMLDEP lib/flags.mli OCAMLDEP lib/segmenttree.mli OCAMLDEP lib/dnet.mli OCAMLDEP lib/envars.mli OCAMLDEP lib/gmapl.mli OCAMLDEP lib/option.mli OCAMLDEP lib/profile.mli OCAMLDEP lib/util.mli OCAMLDEP lib/bstack.mli OCAMLDEP lib/hashcons.mli OCAMLDEP kernel/environ.mli OCAMLDEP kernel/term.mli OCAMLDEP kernel/modops.mli OCAMLDEP kernel/mod_subst.mli OCAMLDEP kernel/inductive.mli OCAMLDEP kernel/sign.mli OCAMLDEP kernel/safe_typing.mli OCAMLDEP kernel/univ.mli OCAMLDEP kernel/cemitcodes.mli OCAMLDEP kernel/esubst.mli OCAMLDEP kernel/pre_env.mli OCAMLDEP kernel/names.mli OCAMLDEP kernel/vm.mli OCAMLDEP kernel/reduction.mli OCAMLDEP kernel/conv_oracle.mli OCAMLDEP kernel/csymtable.mli OCAMLDEP kernel/vconv.mli OCAMLDEP kernel/mod_typing.mli OCAMLDEP kernel/cbytegen.mli OCAMLDEP kernel/closure.mli OCAMLDEP kernel/declarations.mli OCAMLDEP kernel/subtyping.mli OCAMLDEP kernel/typeops.mli OCAMLDEP kernel/term_typing.mli OCAMLDEP kernel/entries.mli OCAMLDEP kernel/cbytecodes.mli OCAMLDEP kernel/retroknowledge.mli OCAMLDEP kernel/type_errors.mli OCAMLDEP kernel/indtypes.mli OCAMLDEP kernel/cooking.mli OCAMLDEP library/library.mli OCAMLDEP library/nameops.mli OCAMLDEP library/heads.mli OCAMLDEP library/global.mli OCAMLDEP library/nametab.mli OCAMLDEP library/summary.mli OCAMLDEP library/assumptions.mli OCAMLDEP library/lib.mli OCAMLDEP library/declaremods.mli OCAMLDEP library/states.mli OCAMLDEP library/impargs.mli OCAMLDEP library/goptions.mli OCAMLDEP library/declare.mli OCAMLDEP library/libnames.mli OCAMLDEP library/dischargedhypsmap.mli OCAMLDEP library/libobject.mli OCAMLDEP library/decls.mli OCAMLDEP library/decl_kinds.mli OCAMLDEP kernel/copcodes.ml OCAMLDEP scripts/tolink.ml OCAMLDEP ide/config_parser.ml OCAMLDEP dev/ocamlweb-doc/syntax.ml OCAMLDEP ide/coq_lex.ml OCAMLDEP ide/highlight.ml OCAMLDEP ide/config_lexer.ml OCAMLDEP ide/utf8_convert.ml OCAMLDEP plugins/dp/dp_zenon.ml OCAMLDEP tools/coqdep_lexer.ml OCAMLDEP tools/coqwc.ml OCAMLDEP tools/coqdoc/cpretty.ml OCAMLDEP tools/gallina_lexer.ml OCAMLDEP dev/ocamlweb-doc/lex.ml OCAMLDEP config/coq_config.ml OCAMLDEP proofs/pfedit.ml OCAMLDEP proofs/refiner.ml OCAMLDEP proofs/tacexpr.ml OCAMLDEP proofs/clenvtac.ml OCAMLDEP proofs/proof_trees.ml OCAMLDEP proofs/tacmach.ml OCAMLDEP proofs/redexpr.ml OCAMLDEP proofs/logic.ml OCAMLDEP proofs/tactic_debug.ml OCAMLDEP proofs/proof_type.ml OCAMLDEP proofs/decl_mode.ml OCAMLDEP proofs/evar_refiner.ml OCAMLDEP interp/genarg.ml OCAMLDEP interp/constrintern.ml OCAMLDEP interp/topconstr.ml OCAMLDEP interp/implicit_quantifiers.ml OCAMLDEP interp/smartlocate.ml OCAMLDEP interp/ppextend.ml OCAMLDEP interp/constrextern.ml OCAMLDEP interp/coqlib.ml OCAMLDEP interp/dumpglob.ml OCAMLDEP interp/notation.ml OCAMLDEP interp/modintern.ml OCAMLDEP interp/reserve.ml OCAMLDEP interp/syntax_def.ml OCAMLDEP myocamlbuild.ml OCAMLDEP parsing/pptactic.ml OCAMLDEP parsing/extend.ml OCAMLDEP parsing/egrammar.ml OCAMLDEP parsing/printmod.ml OCAMLDEP parsing/extrawit.ml OCAMLDEP parsing/prettyp.ml OCAMLDEP parsing/ppvernac.ml OCAMLDEP parsing/ppdecl_proof.ml OCAMLDEP parsing/printer.ml OCAMLDEP parsing/ppconstr.ml OCAMLDEP parsing/tactic_printer.ml OCAMLDEP tactics/decl_proof_instr.ml OCAMLDEP tactics/equality.ml OCAMLDEP tactics/inv.ml OCAMLDEP tactics/dn.ml OCAMLDEP tactics/eqschemes.ml OCAMLDEP tactics/termdn.ml OCAMLDEP tactics/decl_interp.ml OCAMLDEP tactics/evar_tactics.ml OCAMLDEP tactics/hiddentac.ml OCAMLDEP tactics/tactic_option.ml OCAMLDEP tactics/tacinterp.ml OCAMLDEP tactics/btermdn.ml OCAMLDEP tactics/leminv.ml OCAMLDEP tactics/auto.ml OCAMLDEP tactics/dhyp.ml OCAMLDEP tactics/elimschemes.ml OCAMLDEP tactics/tacticals.ml OCAMLDEP tactics/contradiction.ml OCAMLDEP tactics/elim.ml OCAMLDEP tactics/nbtermdn.ml OCAMLDEP tactics/autorewrite.ml OCAMLDEP tactics/refine.ml OCAMLDEP tactics/tactics.ml OCAMLDEP checker/validate.ml OCAMLDEP checker/mod_checking.ml OCAMLDEP checker/reduction.ml OCAMLDEP checker/type_errors.ml OCAMLDEP checker/indtypes.ml OCAMLDEP checker/declarations.ml OCAMLDEP checker/check_stat.ml OCAMLDEP checker/main.ml OCAMLDEP checker/check.ml OCAMLDEP checker/inductive.ml OCAMLDEP checker/subtyping.ml OCAMLDEP checker/checker.ml OCAMLDEP checker/closure.ml OCAMLDEP checker/typeops.ml OCAMLDEP checker/term.ml OCAMLDEP checker/modops.ml OCAMLDEP checker/safe_typing.ml OCAMLDEP checker/environ.ml OCAMLDEP scripts/coqc.ml OCAMLDEP scripts/coqmktop.ml OCAMLDEP ide/ideutils.ml OCAMLDEP ide/coq_tactics.ml OCAMLDEP ide/undo.ml OCAMLDEP ide/tags.ml OCAMLDEP ide/coqide.ml OCAMLDEP ide/gtk_parsing.ml OCAMLDEP ide/utils/configwin_ihm.ml OCAMLDEP ide/utils/configwin_keys.ml OCAMLDEP ide/utils/configwin_types.ml OCAMLDEP ide/utils/editable_cells.ml OCAMLDEP ide/utils/config_file.ml OCAMLDEP ide/utils/configwin_messages.ml OCAMLDEP ide/utils/okey.ml OCAMLDEP ide/utils/configwin.ml OCAMLDEP ide/coq_commands.ml OCAMLDEP ide/coq.ml OCAMLDEP ide/preferences.ml OCAMLDEP ide/command_windows.ml OCAMLDEP ide/typed_notebook.ml OCAMLDEP theories/Numbers/Natural/BigN/NMake_gen.ml OCAMLDEP pretyping/typeclasses.ml OCAMLDEP pretyping/classops.ml OCAMLDEP pretyping/vnorm.ml OCAMLDEP pretyping/indrec.ml OCAMLDEP pretyping/evd.ml OCAMLDEP pretyping/evarconv.ml OCAMLDEP pretyping/rawterm.ml OCAMLDEP pretyping/typeclasses_errors.ml OCAMLDEP pretyping/evarutil.ml OCAMLDEP pretyping/matching.ml OCAMLDEP pretyping/namegen.ml OCAMLDEP pretyping/cbv.ml OCAMLDEP pretyping/retyping.ml OCAMLDEP pretyping/term_dnet.ml OCAMLDEP pretyping/inductiveops.ml OCAMLDEP pretyping/cases.ml OCAMLDEP pretyping/reductionops.ml OCAMLDEP pretyping/unification.ml OCAMLDEP pretyping/termops.ml OCAMLDEP pretyping/clenv.ml OCAMLDEP pretyping/pretyping.ml OCAMLDEP pretyping/pretype_errors.ml OCAMLDEP pretyping/tacred.ml OCAMLDEP pretyping/pattern.ml OCAMLDEP pretyping/typing.ml OCAMLDEP pretyping/coercion.ml OCAMLDEP pretyping/recordops.ml OCAMLDEP pretyping/detyping.ml OCAMLDEP plugins/romega/refl_omega.ml OCAMLDEP plugins/romega/const_omega.ml OCAMLDEP plugins/syntax/numbers_syntax.ml OCAMLDEP plugins/syntax/string_syntax.ml OCAMLDEP plugins/syntax/nat_syntax.ml OCAMLDEP plugins/syntax/r_syntax.ml OCAMLDEP plugins/syntax/z_syntax.ml OCAMLDEP plugins/syntax/ascii_syntax.ml OCAMLDEP plugins/xml/acic.ml OCAMLDEP plugins/xml/unshare.ml OCAMLDEP plugins/xml/cic2acic.ml OCAMLDEP plugins/xml/proof2aproof.ml OCAMLDEP plugins/xml/doubleTypeInference.ml OCAMLDEP plugins/xml/xmlcommand.ml OCAMLDEP plugins/xml/cic2Xml.ml OCAMLDEP plugins/extraction/mlutil.ml OCAMLDEP plugins/extraction/scheme.ml OCAMLDEP plugins/extraction/common.ml OCAMLDEP plugins/extraction/ocaml.ml OCAMLDEP plugins/extraction/extraction.ml OCAMLDEP plugins/extraction/extract_env.ml OCAMLDEP plugins/extraction/modutil.ml OCAMLDEP plugins/extraction/big.ml OCAMLDEP plugins/extraction/table.ml OCAMLDEP plugins/extraction/haskell.ml OCAMLDEP plugins/rtauto/proof_search.ml OCAMLDEP plugins/rtauto/refl_tauto.ml OCAMLDEP plugins/dp/dp.ml OCAMLDEP plugins/dp/dp_why.ml OCAMLDEP plugins/cc/ccalgo.ml OCAMLDEP plugins/cc/cctac.ml OCAMLDEP plugins/cc/ccproof.ml OCAMLDEP plugins/micromega/sos_lib.ml OCAMLDEP plugins/micromega/mutils.ml OCAMLDEP plugins/micromega/persistent_cache.ml OCAMLDEP plugins/micromega/mfourier.ml OCAMLDEP plugins/micromega/sos_types.ml OCAMLDEP plugins/micromega/coq_micromega.ml OCAMLDEP plugins/micromega/sos.ml OCAMLDEP plugins/micromega/csdpcert.ml OCAMLDEP plugins/micromega/certificate.ml OCAMLDEP plugins/micromega/micromega.ml OCAMLDEP plugins/subtac/subtac_errors.ml OCAMLDEP plugins/subtac/subtac_cases.ml OCAMLDEP plugins/subtac/eterm.ml OCAMLDEP plugins/subtac/subtac_obligations.ml OCAMLDEP plugins/subtac/subtac_command.ml OCAMLDEP plugins/subtac/subtac.ml OCAMLDEP plugins/subtac/subtac_classes.ml OCAMLDEP plugins/subtac/subtac_utils.ml OCAMLDEP plugins/subtac/subtac_coercion.ml OCAMLDEP plugins/subtac/subtac_pretyping_F.ml OCAMLDEP plugins/subtac/subtac_pretyping.ml OCAMLDEP plugins/omega/coq_omega.ml OCAMLDEP plugins/omega/omega.ml OCAMLDEP plugins/fourier/fourierR.ml OCAMLDEP plugins/fourier/fourier.ml OCAMLDEP plugins/quote/quote.ml OCAMLDEP plugins/funind/invfun.ml OCAMLDEP plugins/funind/rawtermops.ml OCAMLDEP plugins/funind/functional_principles_types.ml OCAMLDEP plugins/funind/indfun_common.ml OCAMLDEP plugins/funind/merge.ml OCAMLDEP plugins/funind/rawterm_to_relation.ml OCAMLDEP plugins/funind/functional_principles_proofs.ml OCAMLDEP plugins/funind/recdef.ml OCAMLDEP plugins/funind/indfun.ml OCAMLDEP plugins/nsatz/ideal.ml OCAMLDEP plugins/nsatz/polynom.ml OCAMLDEP plugins/nsatz/utile.ml OCAMLDEP plugins/firstorder/unify.ml OCAMLDEP plugins/firstorder/instances.ml OCAMLDEP plugins/firstorder/sequent.ml OCAMLDEP plugins/firstorder/formula.ml OCAMLDEP plugins/firstorder/rules.ml OCAMLDEP plugins/firstorder/ground.ml OCAMLDEP plugins/ring/ring.ml OCAMLDEP tools/coqdep_boot.ml OCAMLDEP tools/coqdep_common.ml OCAMLDEP tools/mkwinapp.ml OCAMLDEP tools/coqdoc/index.ml OCAMLDEP tools/coqdoc/main.ml OCAMLDEP tools/coqdoc/alpha.ml OCAMLDEP tools/coqdoc/cdglobals.ml OCAMLDEP tools/coqdoc/output.ml OCAMLDEP tools/coqdoc/tokens.ml OCAMLDEP tools/coqdep.ml OCAMLDEP tools/gallina.ml OCAMLDEP toplevel/coqtop.ml OCAMLDEP toplevel/indschemes.ml OCAMLDEP toplevel/search.ml OCAMLDEP toplevel/autoinstance.ml OCAMLDEP toplevel/cerrors.ml OCAMLDEP toplevel/auto_ind_decl.ml OCAMLDEP toplevel/vernac.ml OCAMLDEP toplevel/command.ml OCAMLDEP toplevel/vernacentries.ml OCAMLDEP toplevel/ind_tables.ml OCAMLDEP toplevel/vernacinterp.ml OCAMLDEP toplevel/coqinit.ml OCAMLDEP toplevel/record.ml OCAMLDEP toplevel/classes.ml OCAMLDEP toplevel/metasyntax.ml OCAMLDEP toplevel/toplevel.ml OCAMLDEP toplevel/libtypes.ml OCAMLDEP toplevel/vernacexpr.ml OCAMLDEP toplevel/discharge.ml OCAMLDEP toplevel/usage.ml OCAMLDEP toplevel/class.ml OCAMLDEP toplevel/lemmas.ml OCAMLDEP toplevel/himsg.ml OCAMLDEP lib/util.ml OCAMLDEP lib/option.ml OCAMLDEP lib/tries.ml OCAMLDEP lib/unicodetable.ml OCAMLDEP lib/bstack.ml OCAMLDEP lib/bigint.ml OCAMLDEP lib/heap.ml OCAMLDEP lib/rtree.ml OCAMLDEP lib/envars.ml OCAMLDEP lib/dyn.ml OCAMLDEP lib/pp_control.ml OCAMLDEP lib/segmenttree.ml OCAMLDEP lib/gset.ml OCAMLDEP lib/edit.ml OCAMLDEP lib/gmapl.ml OCAMLDEP lib/tlm.ml OCAMLDEP lib/flags.ml OCAMLDEP lib/predicate.ml OCAMLDEP lib/dnet.ml OCAMLDEP lib/fset.ml OCAMLDEP lib/fmap.ml OCAMLDEP lib/system.ml OCAMLDEP lib/gmap.ml OCAMLDEP lib/explore.ml OCAMLDEP lib/hashcons.ml OCAMLDEP lib/profile.ml OCAMLDEP kernel/reduction.ml OCAMLDEP kernel/cbytegen.ml OCAMLDEP kernel/type_errors.ml OCAMLDEP kernel/indtypes.ml OCAMLDEP kernel/declarations.ml OCAMLDEP kernel/esubst.ml OCAMLDEP kernel/cemitcodes.ml OCAMLDEP kernel/mod_subst.ml OCAMLDEP kernel/inductive.ml OCAMLDEP kernel/vm.ml OCAMLDEP kernel/subtyping.ml OCAMLDEP kernel/closure.ml OCAMLDEP kernel/conv_oracle.ml OCAMLDEP kernel/term_typing.ml OCAMLDEP kernel/typeops.ml OCAMLDEP kernel/retroknowledge.ml OCAMLDEP kernel/mod_typing.ml OCAMLDEP kernel/cbytecodes.ml OCAMLDEP kernel/vconv.ml OCAMLDEP kernel/term.ml OCAMLDEP kernel/univ.ml OCAMLDEP kernel/names.ml OCAMLDEP kernel/entries.ml OCAMLDEP kernel/cooking.ml OCAMLDEP kernel/modops.ml OCAMLDEP kernel/safe_typing.ml OCAMLDEP kernel/sign.ml OCAMLDEP kernel/csymtable.ml OCAMLDEP kernel/pre_env.ml OCAMLDEP kernel/environ.ml OCAMLDEP dev/db_printers.ml OCAMLDEP dev/vm_printers.ml OCAMLDEP dev/ocamlweb-doc/parse.ml OCAMLDEP dev/ocamlweb-doc/ast.ml OCAMLDEP dev/top_printers.ml OCAMLDEP library/decl_kinds.ml OCAMLDEP library/assumptions.ml OCAMLDEP library/dischargedhypsmap.ml OCAMLDEP library/libnames.ml OCAMLDEP library/summary.ml OCAMLDEP library/impargs.ml OCAMLDEP library/states.ml OCAMLDEP library/library.ml OCAMLDEP library/decls.ml OCAMLDEP library/nametab.ml OCAMLDEP library/declaremods.ml OCAMLDEP library/libobject.ml OCAMLDEP library/global.ml OCAMLDEP library/nameops.ml OCAMLDEP library/heads.ml OCAMLDEP library/goptions.ml OCAMLDEP library/declare.ml OCAMLDEP library/lib.ml CAMLP4DEPS parsing/g_vernac.ml4 CAMLP4DEPS parsing/g_proofs.ml4 CAMLP4DEPS parsing/g_decl_mode.ml4 CAMLP4DEPS parsing/g_xml.ml4 CAMLP4DEPS tactics/class_tactics.ml4 CAMLP4DEPS tactics/tauto.ml4 CAMLP4DEPS tactics/extraargs.ml4 CAMLP4DEPS tactics/hipattern.ml4 CAMLP4DEPS tactics/eqdecide.ml4 CAMLP4DEPS tactics/rewrite.ml4 CAMLP4DEPS tactics/eauto.ml4 CAMLP4DEPS tactics/extratactics.ml4 CAMLP4DEPS plugins/romega/g_romega.ml4 CAMLP4DEPS plugins/xml/dumptree.ml4 CAMLP4DEPS plugins/xml/acic2Xml.ml4 CAMLP4DEPS plugins/xml/xml.ml4 CAMLP4DEPS plugins/xml/proofTree2Xml.ml4 CAMLP4DEPS plugins/xml/xmlentries.ml4 CAMLP4DEPS plugins/extraction/g_extraction.ml4 CAMLP4DEPS plugins/field/field.ml4 CAMLP4DEPS plugins/rtauto/g_rtauto.ml4 CAMLP4DEPS plugins/dp/g_dp.ml4 CAMLP4DEPS plugins/cc/g_congruence.ml4 CAMLP4DEPS plugins/micromega/g_micromega.ml4 CAMLP4DEPS plugins/subtac/g_subtac.ml4 CAMLP4DEPS plugins/omega/g_omega.ml4 CAMLP4DEPS plugins/fourier/g_fourier.ml4 CAMLP4DEPS plugins/quote/g_quote.ml4 CAMLP4DEPS plugins/setoid_ring/newring.ml4 CAMLP4DEPS plugins/funind/g_indfun.ml4 CAMLP4DEPS plugins/nsatz/nsatz.ml4 CAMLP4DEPS plugins/firstorder/g_ground.ml4 CAMLP4DEPS plugins/ring/g_ring.ml4 CAMLP4DEPS tools/coq_makefile.ml4 CAMLP4DEPS tools/coq_tex.ml4 CAMLP4DEPS toplevel/mltop.ml4 CAMLP4DEPS toplevel/whelp.ml4 CAMLP4DEPS lib/refutpat.ml4 rm tactics/class_tactics.ml plugins/micromega/g_micromega.ml parsing/g_prim.ml plugins/field/field.ml parsing/q_coqast.ml parsing/vernacextend.ml tools/coq_makefile.ml toplevel/whelp.ml plugins/firstorder/g_ground.ml tactics/eauto.ml parsing/g_decl_mode.ml lib/compat.ml plugins/extraction/g_extraction.ml tactics/tauto.ml tactics/hipattern.ml tactics/rewrite.ml plugins/romega/g_romega.ml parsing/g_ltac.ml plugins/xml/xmlentries.ml parsing/q_util.ml parsing/g_tactic.ml plugins/fourier/g_fourier.ml parsing/lexer.ml plugins/funind/g_indfun.ml parsing/pcoq.ml plugins/cc/g_congruence.ml parsing/tacextend.ml plugins/xml/xml.ml plugins/xml/acic2Xml.ml plugins/ring/g_ring.ml plugins/quote/g_quote.ml parsing/g_vernac.ml parsing/g_constr.ml plugins/rtauto/g_rtauto.ml lib/pp.ml plugins/dp/g_dp.ml plugins/omega/g_omega.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml plugins/xml/proofTree2Xml.ml parsing/argextend.ml toplevel/mltop.ml lib/refutpat.ml parsing/q_constr.ml parsing/g_proofs.ml plugins/setoid_ring/newring.ml parsing/g_xml.ml plugins/nsatz/nsatz.ml plugins/subtac/g_subtac.ml tactics/eqdecide.ml tools/coq_tex.ml make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' OCAMLOPT -o bin/coqdep_boot strip bin/coqdep_boot COQDEP parsing/grammar.mllib Testing parsing/grammar.cma OCAMLC -a parsing/grammar.cma OCAMLC lib/pp_control.mli OCAMLC lib/pp.mli OCAMLC4 lib/compat.ml4 OCAMLC lib/util.mli OCAMLC lib/predicate.mli OCAMLC kernel/names.mli OCAMLC kernel/univ.mli OCAMLC kernel/esubst.mli OCAMLC kernel/term.mli OCAMLC kernel/sign.mli OCAMLC kernel/mod_subst.mli OCAMLC library/libnames.mli OCAMLC library/nametab.mli OCAMLC library/summary.mli OCAMLC library/libobject.mli OCAMLC library/lib.mli OCAMLC kernel/cbytecodes.mli OCAMLC kernel/retroknowledge.mli OCAMLC lib/rtree.mli OCAMLC kernel/cemitcodes.mli OCAMLC kernel/declarations.mli OCAMLC kernel/pre_env.mli OCAMLC kernel/environ.mli OCAMLC kernel/closure.mli OCAMLC kernel/reduction.mli OCAMLC pretyping/termops.mli OCAMLC lib/dyn.mli OCAMLC pretyping/evd.mli OCAMLC pretyping/rawterm.mli OCAMLC lib/bigint.mli OCAMLC interp/topconstr.mli OCAMLC pretyping/pattern.mli OCAMLC interp/ppextend.mli OCAMLC library/decl_kinds.mli OCAMLC pretyping/classops.mli OCAMLC interp/notation.mli OCAMLC interp/genarg.mli OCAMLC proofs/tacexpr.ml OCAMLC lib/option.mli OCAMLC library/goptions.mli OCAMLC lib/flags.mli OCAMLC parsing/extend.mli OCAMLC proofs/decl_expr.mli OCAMLC kernel/conv_oracle.mli OCAMLC toplevel/vernacexpr.ml OCAMLC parsing/pcoq.mli OCAMLC parsing/q_util.mli OCAMLC4 parsing/q_constr.ml4 make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' ***************************************************** ***************************************************** ****************** Entering stage2 ****************** ***************************************************** ***************************************************** /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage2 "refman" make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' COQDEP plugins/extraction/ExtrOcamlString.v COQDEP plugins/extraction/ExtrOcamlZBigInt.v COQDEP plugins/extraction/ExtrOcamlZInt.v COQDEP plugins/extraction/ExtrOcamlNatBigInt.v COQDEP plugins/extraction/ExtrOcamlNatInt.v COQDEP plugins/extraction/ExtrOcamlBigIntConv.v COQDEP plugins/extraction/ExtrOcamlIntConv.v COQDEP plugins/extraction/ExtrOcamlBasic.v COQDEP plugins/nsatz/Nsatz.v COQDEP plugins/quote/Quote.v COQDEP plugins/dp/Dp.v COQDEP plugins/setoid_ring/ZArithRing.v COQDEP plugins/setoid_ring/Ring.v COQDEP plugins/setoid_ring/Ring_theory.v COQDEP plugins/setoid_ring/Ring_tac.v COQDEP plugins/setoid_ring/Ring_polynom.v COQDEP plugins/setoid_ring/Ring_equiv.v COQDEP plugins/setoid_ring/Ring_base.v COQDEP plugins/setoid_ring/RealField.v COQDEP plugins/setoid_ring/NArithRing.v COQDEP plugins/setoid_ring/InitialRing.v COQDEP plugins/setoid_ring/Field.v COQDEP plugins/setoid_ring/Field_theory.v COQDEP plugins/setoid_ring/Field_tac.v COQDEP plugins/setoid_ring/BinList.v COQDEP plugins/setoid_ring/ArithRing.v COQDEP plugins/rtauto/Rtauto.v COQDEP plugins/rtauto/Bintree.v COQDEP plugins/funind/Recdef.v COQDEP plugins/fourier/Fourier.v COQDEP plugins/fourier/Fourier_util.v COQDEP plugins/field/LegacyField.v COQDEP plugins/field/LegacyField_Theory.v COQDEP plugins/field/LegacyField_Tactic.v COQDEP plugins/field/LegacyField_Compl.v COQDEP plugins/ring/Setoid_ring.v COQDEP plugins/ring/Setoid_ring_theory.v COQDEP plugins/ring/Setoid_ring_normalize.v COQDEP plugins/ring/Ring_normalize.v COQDEP plugins/ring/Ring_abstract.v COQDEP plugins/ring/LegacyZArithRing.v COQDEP plugins/ring/LegacyRing.v COQDEP plugins/ring/LegacyRing_theory.v COQDEP plugins/ring/LegacyNArithRing.v COQDEP plugins/ring/LegacyArithRing.v COQDEP plugins/micromega/ZMicromega.v COQDEP plugins/micromega/ZCoeff.v COQDEP plugins/micromega/VarMap.v COQDEP plugins/micromega/Tauto.v COQDEP plugins/micromega/RMicromega.v COQDEP plugins/micromega/RingMicromega.v COQDEP plugins/micromega/Refl.v COQDEP plugins/micromega/QMicromega.v COQDEP plugins/micromega/Psatz.v COQDEP plugins/micromega/OrderedRing.v COQDEP plugins/micromega/Env.v COQDEP plugins/micromega/EnvRing.v COQDEP plugins/micromega/CheckerMaker.v COQDEP plugins/romega/ROmega.v COQDEP plugins/romega/ReflOmegaCore.v COQDEP plugins/omega/PreOmega.v COQDEP plugins/omega/Omega.v COQDEP plugins/omega/OmegaPlugin.v COQDEP plugins/omega/OmegaLemmas.v COQDEP theories/Structures/OrderedType.v COQDEP theories/Structures/OrderedTypeEx.v COQDEP theories/Structures/OrderedTypeAlt.v COQDEP theories/Structures/DecidableTypeEx.v COQDEP theories/Structures/DecidableType.v COQDEP theories/Structures/GenericMinMax.v COQDEP theories/Structures/OrdersAlt.v COQDEP theories/Structures/OrdersTac.v COQDEP theories/Structures/OrdersLists.v COQDEP theories/Structures/OrdersFacts.v COQDEP theories/Structures/OrdersEx.v COQDEP theories/Structures/Orders.v COQDEP theories/Structures/EqualitiesFacts.v COQDEP theories/Structures/Equalities.v COQDEP theories/Program/Wf.v COQDEP theories/Program/Utils.v COQDEP theories/Program/Tactics.v COQDEP theories/Program/Syntax.v COQDEP theories/Program/Subset.v COQDEP theories/Program/Program.v COQDEP theories/Program/Equality.v COQDEP theories/Program/Combinators.v COQDEP theories/Program/Basics.v COQDEP theories/Classes/RelationPairs.v COQDEP theories/Classes/SetoidTactics.v COQDEP theories/Classes/SetoidDec.v COQDEP theories/Classes/SetoidClass.v COQDEP theories/Classes/RelationClasses.v COQDEP theories/Classes/Morphisms.v COQDEP theories/Classes/Morphisms_Relations.v COQDEP theories/Classes/Morphisms_Prop.v COQDEP theories/Classes/Init.v COQDEP theories/Classes/EquivDec.v COQDEP theories/Classes/Equivalence.v COQDEP theories/Unicode/Utf8_core.v COQDEP theories/Unicode/Utf8.v COQDEP theories/Numbers/Rational/SpecViaQ/QSig.v COQDEP theories/Numbers/Rational/BigQ/QMake.v COQDEP theories/Numbers/Rational/BigQ/BigQ.v COQDEP theories/Numbers/NumPrelude.v COQDEP theories/Numbers/Natural/SpecViaZ/NSig.v COQDEP theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v COQDEP theories/Numbers/Natural/Peano/NPeano.v COQDEP theories/Numbers/Natural/Binary/NBinary.v COQDEP theories/Numbers/Natural/BigN/NMake.v COQDEP theories/Numbers/Natural/BigN/NMake_gen.v COQDEP theories/Numbers/Natural/BigN/Nbasic.v COQDEP theories/Numbers/Natural/BigN/BigN.v COQDEP theories/Numbers/Natural/Abstract/NDiv.v COQDEP theories/Numbers/Natural/Abstract/NProperties.v COQDEP theories/Numbers/Natural/Abstract/NSub.v COQDEP theories/Numbers/Natural/Abstract/NStrongRec.v COQDEP theories/Numbers/Natural/Abstract/NOrder.v COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v COQDEP theories/Numbers/Natural/Abstract/NIso.v COQDEP theories/Numbers/Natural/Abstract/NDefOps.v COQDEP theories/Numbers/Natural/Abstract/NBase.v COQDEP theories/Numbers/Natural/Abstract/NAxioms.v COQDEP theories/Numbers/Natural/Abstract/NAdd.v COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v COQDEP theories/Numbers/NatInt/NZDiv.v COQDEP theories/Numbers/NatInt/NZDomain.v COQDEP theories/Numbers/NatInt/NZProperties.v COQDEP theories/Numbers/NatInt/NZOrder.v COQDEP theories/Numbers/NatInt/NZMul.v COQDEP theories/Numbers/NatInt/NZMulOrder.v COQDEP theories/Numbers/NatInt/NZBase.v COQDEP theories/Numbers/NatInt/NZAxioms.v COQDEP theories/Numbers/NatInt/NZAdd.v COQDEP theories/Numbers/NatInt/NZAddOrder.v COQDEP theories/Numbers/NaryFunctions.v COQDEP theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v COQDEP theories/Numbers/Integer/SpecViaZ/ZSig.v COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v COQDEP theories/Numbers/Integer/Binary/ZBinary.v COQDEP theories/Numbers/Integer/BigZ/ZMake.v COQDEP theories/Numbers/Integer/BigZ/BigZ.v COQDEP theories/Numbers/Integer/Abstract/ZDivEucl.v COQDEP theories/Numbers/Integer/Abstract/ZDivTrunc.v COQDEP theories/Numbers/Integer/Abstract/ZDivFloor.v COQDEP theories/Numbers/Integer/Abstract/ZProperties.v COQDEP theories/Numbers/Integer/Abstract/ZSgnAbs.v COQDEP theories/Numbers/Integer/Abstract/ZMul.v COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v COQDEP theories/Numbers/Integer/Abstract/ZLt.v COQDEP theories/Numbers/Integer/Abstract/ZBase.v COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v COQDEP theories/Numbers/Integer/Abstract/ZAdd.v COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v COQDEP theories/Numbers/Cyclic/Int31/Ring31.v COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v COQDEP theories/Numbers/Cyclic/Int31/Int31.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQDEP theories/Numbers/BigNumPrelude.v COQDEP theories/QArith/Qminmax.v COQDEP theories/QArith/QOrderedType.v COQDEP theories/QArith/Qround.v COQDEP theories/QArith/Qring.v COQDEP theories/QArith/Qreduction.v COQDEP theories/QArith/Qreals.v COQDEP theories/QArith/Qpower.v COQDEP theories/QArith/Qfield.v COQDEP theories/QArith/Qcanon.v COQDEP theories/QArith/QArith.v COQDEP theories/QArith/QArith_base.v COQDEP theories/QArith/Qabs.v COQDEP theories/Sorting/Mergesort.v COQDEP theories/Sorting/Sorting.v COQDEP theories/Sorting/Sorted.v COQDEP theories/Sorting/PermutEq.v COQDEP theories/Sorting/PermutSetoid.v COQDEP theories/Sorting/Permutation.v COQDEP theories/Sorting/Heap.v COQDEP theories/Reals/Rminmax.v COQDEP theories/Reals/ROrderedType.v COQDEP theories/Reals/Sqrt_reg.v COQDEP theories/Reals/SplitRmult.v COQDEP theories/Reals/SplitAbsolu.v COQDEP theories/Reals/SeqSeries.v COQDEP theories/Reals/SeqProp.v COQDEP theories/Reals/Rtrigo.v COQDEP theories/Reals/Rtrigo_reg.v COQDEP theories/Reals/Rtrigo_fun.v COQDEP theories/Reals/Rtrigo_def.v COQDEP theories/Reals/Rtrigo_calc.v COQDEP theories/Reals/Rtrigo_alt.v COQDEP theories/Reals/Rtopology.v COQDEP theories/Reals/R_sqr.v COQDEP theories/Reals/R_sqrt.v COQDEP theories/Reals/Rsqrt_def.v COQDEP theories/Reals/Rsigma.v COQDEP theories/Reals/Rseries.v COQDEP theories/Reals/Rprod.v COQDEP theories/Reals/Rpower.v COQDEP theories/Reals/Rpow_def.v COQDEP theories/Reals/Rlogic.v COQDEP theories/Reals/RList.v COQDEP theories/Reals/Rlimit.v COQDEP theories/Reals/RIneq.v COQDEP theories/Reals/R_Ifp.v COQDEP theories/Reals/RiemannInt.v COQDEP theories/Reals/RiemannInt_SF.v COQDEP theories/Reals/Rgeom.v COQDEP theories/Reals/Rfunctions.v COQDEP theories/Reals/Reals.v COQDEP theories/Reals/Rderiv.v COQDEP theories/Reals/Rdefinitions.v COQDEP theories/Reals/Rcomplete.v COQDEP theories/Reals/Rbasic_fun.v COQDEP theories/Reals/Rbase.v COQDEP theories/Reals/Raxioms.v COQDEP theories/Reals/Ranalysis.v COQDEP theories/Reals/Ranalysis4.v COQDEP theories/Reals/Ranalysis3.v COQDEP theories/Reals/Ranalysis2.v COQDEP theories/Reals/Ranalysis1.v COQDEP theories/Reals/PSeries_reg.v COQDEP theories/Reals/PartSum.v COQDEP theories/Reals/NewtonInt.v COQDEP theories/Reals/MVT.v COQDEP theories/Reals/LegacyRfield.v COQDEP theories/Reals/Integration.v COQDEP theories/Reals/Exp_prop.v COQDEP theories/Reals/DiscrR.v COQDEP theories/Reals/Cos_rel.v COQDEP theories/Reals/Cos_plus.v COQDEP theories/Reals/Cauchy_prod.v COQDEP theories/Reals/Binomial.v COQDEP theories/Reals/ArithProp.v COQDEP theories/Reals/AltSeries.v COQDEP theories/Reals/Alembert.v COQDEP theories/Wellfounded/Well_Ordering.v COQDEP theories/Wellfounded/Wellfounded.v COQDEP theories/Wellfounded/Union.v COQDEP theories/Wellfounded/Transitive_Closure.v COQDEP theories/Wellfounded/Lexicographic_Product.v COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v COQDEP theories/Wellfounded/Inverse_Image.v COQDEP theories/Wellfounded/Inclusion.v COQDEP theories/Wellfounded/Disjoint_Union.v COQDEP theories/Relations/Relations.v COQDEP theories/Relations/Relation_Operators.v COQDEP theories/Relations/Relation_Definitions.v COQDEP theories/Relations/Operators_Properties.v COQDEP theories/MSets/MSetPositive.v COQDEP theories/MSets/MSetWeakList.v COQDEP theories/MSets/MSetToFiniteSet.v COQDEP theories/MSets/MSets.v COQDEP theories/MSets/MSetProperties.v COQDEP theories/MSets/MSetList.v COQDEP theories/MSets/MSetInterface.v COQDEP theories/MSets/MSetFacts.v COQDEP theories/MSets/MSetEqProperties.v COQDEP theories/MSets/MSetDecide.v COQDEP theories/MSets/MSetAVL.v COQDEP theories/FSets/FSetWeakList.v COQDEP theories/FSets/FSetToFiniteSet.v COQDEP theories/FSets/FSets.v COQDEP theories/FSets/FSetProperties.v COQDEP theories/FSets/FSetList.v COQDEP theories/FSets/FSetInterface.v COQDEP theories/FSets/FSetFacts.v COQDEP theories/FSets/FSetEqProperties.v COQDEP theories/FSets/FSetDecide.v COQDEP theories/FSets/FSetBridge.v COQDEP theories/FSets/FSetPositive.v COQDEP theories/FSets/FSetAVL.v COQDEP theories/FSets/FSetCompat.v COQDEP theories/FSets/FMapWeakList.v COQDEP theories/FSets/FMaps.v COQDEP theories/FSets/FMapPositive.v COQDEP theories/FSets/FMapList.v COQDEP theories/FSets/FMapInterface.v COQDEP theories/FSets/FMapFullAVL.v COQDEP theories/FSets/FMapFacts.v COQDEP theories/FSets/FMapAVL.v COQDEP theories/Sets/Uniset.v COQDEP theories/Sets/Relations_3.v COQDEP theories/Sets/Relations_3_facts.v COQDEP theories/Sets/Relations_2.v COQDEP theories/Sets/Relations_2_facts.v COQDEP theories/Sets/Relations_1.v COQDEP theories/Sets/Relations_1_facts.v COQDEP theories/Sets/Powerset.v COQDEP theories/Sets/Powerset_facts.v COQDEP theories/Sets/Powerset_Classical_facts.v COQDEP theories/Sets/Permut.v COQDEP theories/Sets/Partial_Order.v COQDEP theories/Sets/Multiset.v COQDEP theories/Sets/Integers.v COQDEP theories/Sets/Infinite_sets.v COQDEP theories/Sets/Image.v COQDEP theories/Sets/Finite_sets.v COQDEP theories/Sets/Finite_sets_facts.v COQDEP theories/Sets/Ensembles.v COQDEP theories/Sets/Cpo.v COQDEP theories/Sets/Constructive_sets.v COQDEP theories/Sets/Classical_sets.v COQDEP theories/Strings/String.v COQDEP theories/Strings/Ascii.v COQDEP theories/Lists/TheoryList.v COQDEP theories/Lists/Streams.v COQDEP theories/Lists/StreamMemo.v COQDEP theories/Lists/SetoidList.v COQDEP theories/Lists/List.v COQDEP theories/Lists/ListTactics.v COQDEP theories/Lists/ListSet.v COQDEP theories/Setoids/Setoid.v COQDEP theories/ZArith/ZOrderedType.v COQDEP theories/ZArith/Zwf.v COQDEP theories/ZArith/Zsqrt.v COQDEP theories/ZArith/Zpow_facts.v COQDEP theories/ZArith/Zpower.v COQDEP theories/ZArith/Zpow_def.v COQDEP theories/ZArith/Zorder.v COQDEP theories/ZArith/ZOdiv.v COQDEP theories/ZArith/ZOdiv_def.v COQDEP theories/ZArith/Znumtheory.v COQDEP theories/ZArith/Znat.v COQDEP theories/ZArith/Zmisc.v COQDEP theories/ZArith/Zmin.v COQDEP theories/ZArith/Zminmax.v COQDEP theories/ZArith/Zmax.v COQDEP theories/ZArith/Zlogarithm.v COQDEP theories/ZArith/Zhints.v COQDEP theories/ZArith/Zgcd_alt.v COQDEP theories/ZArith/Zeven.v COQDEP theories/ZArith/Zdiv.v COQDEP theories/ZArith/Zcomplements.v COQDEP theories/ZArith/Zcompare.v COQDEP theories/ZArith/Zbool.v COQDEP theories/ZArith/Zdigits.v COQDEP theories/ZArith/ZArith.v COQDEP theories/ZArith/ZArith_dec.v COQDEP theories/ZArith/ZArith_base.v COQDEP theories/ZArith/Zabs.v COQDEP theories/ZArith/Wf_Z.v COQDEP theories/ZArith/Int.v COQDEP theories/ZArith/BinInt.v COQDEP theories/ZArith/auxiliary.v COQDEP theories/NArith/Nminmax.v COQDEP theories/NArith/NOrderedType.v COQDEP theories/NArith/Pminmax.v COQDEP theories/NArith/POrderedType.v COQDEP theories/NArith/Pnat.v COQDEP theories/NArith/Nnat.v COQDEP theories/NArith/Ndist.v COQDEP theories/NArith/Ndigits.v COQDEP theories/NArith/Ndec.v COQDEP theories/NArith/NArith.v COQDEP theories/NArith/BinPos.v COQDEP theories/NArith/BinNat.v COQDEP theories/Bool/Zerob.v COQDEP theories/Bool/Sumbool.v COQDEP theories/Bool/IfProp.v COQDEP theories/Bool/DecBool.v COQDEP theories/Bool/Bvector.v COQDEP theories/Bool/Bool.v COQDEP theories/Bool/BoolEq.v COQDEP theories/Arith/MinMax.v COQDEP theories/Arith/NatOrderedType.v COQDEP theories/Arith/Wf_nat.v COQDEP theories/Arith/Plus.v COQDEP theories/Arith/Peano_dec.v COQDEP theories/Arith/Mult.v COQDEP theories/Arith/Min.v COQDEP theories/Arith/Minus.v COQDEP theories/Arith/Max.v COQDEP theories/Arith/Lt.v COQDEP theories/Arith/Le.v COQDEP theories/Arith/Gt.v COQDEP theories/Arith/Factorial.v COQDEP theories/Arith/Even.v COQDEP theories/Arith/Euclid.v COQDEP theories/Arith/EqNat.v COQDEP theories/Arith/Div2.v COQDEP theories/Arith/Compare.v COQDEP theories/Arith/Compare_dec.v COQDEP theories/Arith/Bool_nat.v COQDEP theories/Arith/Between.v COQDEP theories/Arith/Arith.v COQDEP theories/Arith/Arith_base.v COQDEP theories/Logic/SetIsType.v COQDEP theories/Logic/RelationalChoice.v COQDEP theories/Logic/ProofIrrelevance.v COQDEP theories/Logic/ProofIrrelevanceFacts.v COQDEP theories/Logic/JMeq.v COQDEP theories/Logic/IndefiniteDescription.v COQDEP theories/Logic/Hurkens.v COQDEP theories/Logic/FunctionalExtensionality.v COQDEP theories/Logic/Eqdep.v COQDEP theories/Logic/EqdepFacts.v COQDEP theories/Logic/Eqdep_dec.v COQDEP theories/Logic/Epsilon.v COQDEP theories/Logic/Diaconescu.v COQDEP theories/Logic/Description.v COQDEP theories/Logic/Decidable.v COQDEP theories/Logic/ConstructiveEpsilon.v COQDEP theories/Logic/Classical.v COQDEP theories/Logic/ClassicalUniqueChoice.v COQDEP theories/Logic/Classical_Type.v COQDEP theories/Logic/Classical_Prop.v COQDEP theories/Logic/Classical_Pred_Type.v COQDEP theories/Logic/Classical_Pred_Set.v COQDEP theories/Logic/ClassicalFacts.v COQDEP theories/Logic/ClassicalEpsilon.v COQDEP theories/Logic/ClassicalDescription.v COQDEP theories/Logic/ClassicalChoice.v COQDEP theories/Logic/ChoiceFacts.v COQDEP theories/Logic/Berardi.v COQDEP theories/Init/Wf.v COQDEP theories/Init/Tactics.v COQDEP theories/Init/Specif.v COQDEP theories/Init/Prelude.v COQDEP theories/Init/Peano.v COQDEP theories/Init/Notations.v COQDEP theories/Init/Logic.v COQDEP theories/Init/Logic_Type.v COQDEP theories/Init/Datatypes.v OCAMLC config/coq_config.mli OCAMLC config/coq_config.ml OCAMLC lib/profile.mli OCAMLC lib/profile.ml OCAMLC lib/pp_control.ml OCAMLC4 lib/pp.ml4 OCAMLC lib/flags.ml OCAMLC lib/segmenttree.mli OCAMLC lib/segmenttree.ml OCAMLC lib/unicodetable.ml OCAMLC lib/util.ml OCAMLC lib/bigint.ml OCAMLC lib/dyn.ml OCAMLC lib/hashcons.mli OCAMLC lib/hashcons.ml OCAMLC lib/predicate.ml OCAMLC lib/rtree.ml OCAMLC lib/option.ml OCAMLC kernel/names.ml OCAMLC kernel/univ.ml OCAMLC kernel/esubst.ml OCAMLC kernel/term.ml OCAMLC kernel/mod_subst.ml OCAMLC kernel/sign.ml OCAMLC kernel/cbytecodes.ml OCAMLC kernel/copcodes.ml OCAMLC kernel/cemitcodes.ml OCAMLC kernel/declarations.ml OCAMLC kernel/retroknowledge.ml OCAMLC kernel/pre_env.ml OCAMLC kernel/cbytegen.mli OCAMLC kernel/cbytegen.ml OCAMLC kernel/environ.ml OCAMLC kernel/conv_oracle.ml OCAMLC kernel/closure.ml OCAMLC kernel/reduction.ml OCAMLC kernel/type_errors.mli OCAMLC kernel/type_errors.ml OCAMLC kernel/entries.mli OCAMLC kernel/entries.ml OCAMLC kernel/modops.mli OCAMLC kernel/modops.ml OCAMLC kernel/inductive.mli OCAMLC kernel/inductive.ml OCAMLC kernel/typeops.mli OCAMLC kernel/typeops.ml 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 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 library/nameops.mli OCAMLC library/nameops.ml OCAMLC library/libnames.ml OCAMLC library/summary.ml OCAMLC library/nametab.ml OCAMLC library/libobject.ml OCAMLC library/lib.ml OCAMLC library/goptions.ml OCAMLC library/decl_kinds.ml OCAMLC library/global.mli OCAMLC library/global.ml OCAMLC pretyping/termops.ml OCAMLC pretyping/namegen.mli OCAMLC pretyping/namegen.ml OCAMLC pretyping/evd.ml OCAMLC pretyping/reductionops.mli OCAMLC pretyping/reductionops.ml OCAMLC pretyping/inductiveops.mli OCAMLC pretyping/inductiveops.ml OCAMLC pretyping/rawterm.ml OCAMLC pretyping/detyping.mli OCAMLC pretyping/detyping.ml OCAMLC pretyping/pattern.ml OCAMLC interp/topconstr.ml OCAMLC interp/genarg.ml OCAMLC interp/ppextend.ml OCAMLC parsing/lexer.mli OCAMLC4 parsing/lexer.ml4 OCAMLC parsing/extend.ml OCAMLC parsing/extrawit.mli OCAMLC parsing/extrawit.ml OCAMLC4 parsing/pcoq.ml4 OCAMLC4 parsing/q_util.ml4 OCAMLC4 parsing/q_coqast.ml4 OCAMLC parsing/egrammar.mli OCAMLC parsing/egrammar.ml OCAMLC4 parsing/argextend.ml4 OCAMLC4 parsing/tacextend.ml4 OCAMLC4 parsing/vernacextend.ml4 OCAMLC4 parsing/g_prim.ml4 OCAMLC4 parsing/g_tactic.ml4 OCAMLC4 parsing/g_ltac.ml4 OCAMLC4 parsing/g_constr.ml4 Testing parsing/grammar.cma OCAMLC -a parsing/grammar.cma TOUCH lib/pp.ml TOUCH lib/compat.ml TOUCH lib/refutpat.ml TOUCH toplevel/whelp.ml TOUCH toplevel/mltop.ml TOUCH tools/coq_tex.ml TOUCH tools/coq_makefile.ml TOUCH plugins/ring/g_ring.ml TOUCH plugins/firstorder/g_ground.ml TOUCH plugins/nsatz/nsatz.ml TOUCH plugins/funind/g_indfun.ml TOUCH plugins/setoid_ring/newring.ml TOUCH plugins/quote/g_quote.ml TOUCH plugins/fourier/g_fourier.ml TOUCH plugins/omega/g_omega.ml TOUCH plugins/subtac/g_subtac.ml TOUCH plugins/micromega/g_micromega.ml TOUCH plugins/cc/g_congruence.ml TOUCH plugins/dp/g_dp.ml TOUCH plugins/rtauto/g_rtauto.ml TOUCH plugins/field/field.ml TOUCH plugins/extraction/g_extraction.ml TOUCH plugins/xml/xmlentries.ml TOUCH plugins/xml/proofTree2Xml.ml TOUCH plugins/xml/xml.ml TOUCH plugins/xml/acic2Xml.ml TOUCH plugins/xml/dumptree.ml TOUCH plugins/romega/g_romega.ml TOUCH tactics/extratactics.ml TOUCH tactics/eauto.ml TOUCH tactics/rewrite.ml TOUCH tactics/eqdecide.ml TOUCH tactics/hipattern.ml TOUCH tactics/extraargs.ml TOUCH tactics/tauto.ml TOUCH tactics/class_tactics.ml TOUCH parsing/vernacextend.ml TOUCH parsing/g_constr.ml TOUCH parsing/q_constr.ml TOUCH parsing/g_xml.ml TOUCH parsing/g_decl_mode.ml TOUCH parsing/tacextend.ml TOUCH parsing/q_util.ml TOUCH parsing/g_ltac.ml TOUCH parsing/q_coqast.ml TOUCH parsing/g_tactic.ml TOUCH parsing/g_proofs.ml TOUCH parsing/g_vernac.ml TOUCH parsing/lexer.ml TOUCH parsing/argextend.ml TOUCH parsing/g_prim.ml TOUCH parsing/pcoq.ml OCAMLDEP4 parsing/g_vernac.ml4 OCAMLDEP4 parsing/g_proofs.ml4 OCAMLDEP4 parsing/g_decl_mode.ml4 OCAMLDEP4 parsing/g_xml.ml4 OCAMLDEP4 tactics/class_tactics.ml4 OCAMLDEP4 tactics/tauto.ml4 OCAMLDEP4 tactics/extraargs.ml4 OCAMLDEP4 tactics/hipattern.ml4 OCAMLDEP4 tactics/eqdecide.ml4 OCAMLDEP4 tactics/rewrite.ml4 OCAMLDEP4 tactics/eauto.ml4 OCAMLDEP4 tactics/extratactics.ml4 OCAMLDEP4 plugins/romega/g_romega.ml4 OCAMLDEP4 plugins/xml/dumptree.ml4 OCAMLDEP4 plugins/xml/acic2Xml.ml4 OCAMLDEP4 plugins/xml/xml.ml4 OCAMLDEP4 plugins/xml/proofTree2Xml.ml4 OCAMLDEP4 plugins/xml/xmlentries.ml4 OCAMLDEP4 plugins/extraction/g_extraction.ml4 OCAMLDEP4 plugins/field/field.ml4 OCAMLDEP4 plugins/rtauto/g_rtauto.ml4 OCAMLDEP4 plugins/dp/g_dp.ml4 OCAMLDEP4 plugins/cc/g_congruence.ml4 OCAMLDEP4 plugins/micromega/g_micromega.ml4 OCAMLDEP4 plugins/subtac/g_subtac.ml4 OCAMLDEP4 plugins/omega/g_omega.ml4 OCAMLDEP4 plugins/fourier/g_fourier.ml4 OCAMLDEP4 plugins/quote/g_quote.ml4 OCAMLDEP4 plugins/setoid_ring/newring.ml4 OCAMLDEP4 plugins/funind/g_indfun.ml4 OCAMLDEP4 plugins/nsatz/nsatz.ml4 OCAMLDEP4 plugins/firstorder/g_ground.ml4 OCAMLDEP4 plugins/ring/g_ring.ml4 OCAMLDEP4 tools/coq_makefile.ml4 OCAMLDEP4 tools/coq_tex.ml4 OCAMLDEP4 toplevel/mltop.ml4 OCAMLDEP4 toplevel/whelp.ml4 OCAMLDEP4 lib/refutpat.ml4 ECHO... > plugins/romega/romega_plugin_mod.ml OCAMLDEP plugins/romega/romega_plugin_mod.ml ECHO... > plugins/syntax/z_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/z_syntax_plugin_mod.ml ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/nat_syntax_plugin_mod.ml ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/ascii_syntax_plugin_mod.ml ECHO... > plugins/syntax/r_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/r_syntax_plugin_mod.ml ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/numbers_syntax_plugin_mod.ml ECHO... > plugins/syntax/string_syntax_plugin_mod.ml OCAMLDEP plugins/syntax/string_syntax_plugin_mod.ml ECHO... > plugins/xml/xml_plugin_mod.ml OCAMLDEP plugins/xml/xml_plugin_mod.ml ECHO... > plugins/extraction/extraction_plugin_mod.ml OCAMLDEP plugins/extraction/extraction_plugin_mod.ml ECHO... > plugins/field/field_plugin_mod.ml OCAMLDEP plugins/field/field_plugin_mod.ml ECHO... > plugins/rtauto/rtauto_plugin_mod.ml OCAMLDEP plugins/rtauto/rtauto_plugin_mod.ml ECHO... > plugins/dp/dp_plugin_mod.ml OCAMLDEP plugins/dp/dp_plugin_mod.ml ECHO... > plugins/cc/cc_plugin_mod.ml OCAMLDEP plugins/cc/cc_plugin_mod.ml ECHO... > plugins/micromega/micromega_plugin_mod.ml OCAMLDEP plugins/micromega/micromega_plugin_mod.ml ECHO... > plugins/subtac/subtac_plugin_mod.ml OCAMLDEP plugins/subtac/subtac_plugin_mod.ml ECHO... > plugins/omega/omega_plugin_mod.ml OCAMLDEP plugins/omega/omega_plugin_mod.ml ECHO... > plugins/fourier/fourier_plugin_mod.ml OCAMLDEP plugins/fourier/fourier_plugin_mod.ml ECHO... > plugins/quote/quote_plugin_mod.ml OCAMLDEP plugins/quote/quote_plugin_mod.ml ECHO... > plugins/setoid_ring/newring_plugin_mod.ml OCAMLDEP plugins/setoid_ring/newring_plugin_mod.ml ECHO... > plugins/funind/recdef_plugin_mod.ml OCAMLDEP plugins/funind/recdef_plugin_mod.ml ECHO... > plugins/nsatz/nsatz_plugin_mod.ml OCAMLDEP plugins/nsatz/nsatz_plugin_mod.ml ECHO... > plugins/firstorder/ground_plugin_mod.ml OCAMLDEP plugins/firstorder/ground_plugin_mod.ml ECHO... > plugins/ring/ring_plugin_mod.ml OCAMLDEP plugins/ring/ring_plugin_mod.ml COQDEP proofs/proofs.mllib COQDEP interp/interp.mllib COQDEP parsing/highparsing.mllib COQDEP parsing/parsing.mllib COQDEP tactics/tactics.mllib COQDEP tactics/hightactics.mllib COQDEP checker/check.mllib COQDEP ide/ide.mllib COQDEP pretyping/pretyping.mllib COQDEP plugins/romega/romega_plugin.mllib COQDEP plugins/syntax/z_syntax_plugin.mllib COQDEP plugins/syntax/nat_syntax_plugin.mllib COQDEP plugins/syntax/ascii_syntax_plugin.mllib COQDEP plugins/syntax/r_syntax_plugin.mllib COQDEP plugins/syntax/numbers_syntax_plugin.mllib COQDEP plugins/syntax/string_syntax_plugin.mllib COQDEP plugins/xml/xml_plugin.mllib COQDEP plugins/extraction/extraction_plugin.mllib COQDEP plugins/field/field_plugin.mllib COQDEP plugins/rtauto/rtauto_plugin.mllib COQDEP plugins/dp/dp_plugin.mllib COQDEP plugins/cc/cc_plugin.mllib COQDEP plugins/micromega/micromega_plugin.mllib COQDEP plugins/subtac/subtac_plugin.mllib COQDEP plugins/omega/omega_plugin.mllib COQDEP plugins/fourier/fourier_plugin.mllib COQDEP plugins/quote/quote_plugin.mllib COQDEP plugins/setoid_ring/newring_plugin.mllib COQDEP plugins/funind/recdef_plugin.mllib COQDEP plugins/nsatz/nsatz_plugin.mllib COQDEP plugins/firstorder/ground_plugin.mllib COQDEP plugins/ring/ring_plugin.mllib COQDEP toplevel/toplevel.mllib COQDEP lib/lib.mllib COQDEP kernel/kernel.mllib COQDEP dev/printers.mllib COQDEP library/library.mllib rm tactics/tauto.ml tactics/class_tactics.ml plugins/micromega/g_micromega.ml tools/coq_tex.ml plugins/field/field.ml parsing/vernacextend.ml toplevel/whelp.ml tactics/eauto.ml plugins/omega/g_omega.ml tactics/rewrite.ml plugins/romega/g_romega.ml parsing/g_ltac.ml plugins/xml/xmlentries.ml tactics/hipattern.ml parsing/g_tactic.ml parsing/lexer.ml parsing/tacextend.ml plugins/quote/g_quote.ml plugins/fourier/g_fourier.ml lib/pp.ml plugins/dp/g_dp.ml parsing/g_proofs.ml plugins/xml/proofTree2Xml.ml parsing/g_decl_mode.ml toplevel/mltop.ml lib/refutpat.ml parsing/q_constr.ml plugins/cc/g_congruence.ml plugins/xml/acic2Xml.ml plugins/funind/g_indfun.ml parsing/g_prim.ml parsing/q_coqast.ml plugins/extraction/g_extraction.ml lib/compat.ml parsing/g_vernac.ml parsing/g_constr.ml parsing/pcoq.ml plugins/xml/xml.ml plugins/firstorder/g_ground.ml plugins/ring/g_ring.ml parsing/g_xml.ml plugins/subtac/g_subtac.ml plugins/rtauto/g_rtauto.ml plugins/xml/dumptree.ml tactics/extraargs.ml tactics/extratactics.ml parsing/argextend.ml plugins/setoid_ring/newring.ml plugins/nsatz/nsatz.ml parsing/q_util.ml tools/coq_makefile.ml tactics/eqdecide.ml make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' install -m 644 doc/common/styles/html/simple/styles.hva doc/refman OCAMLOPT4 tools/coq_tex.ml4 OCAMLOPT -o bin/coq-tex strip bin/coq-tex OCAMLOPT config/coq_config.ml OCAMLOPT lib/pp_control.ml OCAMLOPT4 lib/pp.ml4 OCAMLOPT4 lib/compat.ml4 OCAMLOPT lib/flags.ml OCAMLOPT lib/segmenttree.ml OCAMLOPT lib/unicodetable.ml OCAMLOPT lib/util.ml OCAMLC lib/system.mli OCAMLOPT lib/system.ml OCAMLC lib/envars.mli OCAMLOPT lib/envars.ml OCAMLOPT scripts/tolink.ml OCAMLOPT scripts/coqmktop.ml OCAMLOPT -o bin/coqmktop.opt strip bin/coqmktop.opt cd bin; ln -sf coqmktop.opt coqmktop OCAMLOPT lib/bigint.ml OCAMLOPT lib/hashcons.ml OCAMLOPT lib/dyn.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/fset.mli OCAMLOPT lib/fset.ml OCAMLC lib/fmap.mli OCAMLOPT lib/fmap.ml OCAMLC lib/tlm.mli OCAMLOPT lib/tlm.ml OCAMLC lib/tries.mli OCAMLOPT lib/tries.ml OCAMLC lib/gmapl.mli OCAMLOPT lib/gmapl.ml OCAMLOPT lib/profile.ml OCAMLC lib/explore.mli OCAMLOPT lib/explore.ml OCAMLOPT lib/predicate.ml OCAMLOPT lib/rtree.ml OCAMLC lib/heap.mli OCAMLOPT lib/heap.ml OCAMLOPT lib/option.ml OCAMLC lib/dnet.mli OCAMLOPT lib/dnet.ml OCAMLOPT -a -o lib/lib.cmxa OCAMLOPT kernel/names.ml OCAMLOPT kernel/univ.ml OCAMLOPT kernel/esubst.ml OCAMLOPT kernel/term.ml OCAMLOPT kernel/mod_subst.ml OCAMLOPT kernel/sign.ml OCAMLOPT kernel/cbytecodes.ml OCAMLOPT kernel/copcodes.ml OCAMLOPT kernel/cemitcodes.ml OCAMLOPT kernel/retroknowledge.ml OCAMLOPT kernel/declarations.ml OCAMLOPT kernel/pre_env.ml OCAMLOPT kernel/cbytegen.ml OCAMLOPT kernel/environ.ml OCAMLOPT kernel/conv_oracle.ml OCAMLOPT kernel/closure.ml OCAMLOPT kernel/reduction.ml OCAMLOPT kernel/type_errors.ml OCAMLOPT kernel/entries.ml OCAMLOPT kernel/modops.ml OCAMLOPT kernel/inductive.ml OCAMLOPT kernel/typeops.ml OCAMLOPT kernel/indtypes.ml OCAMLOPT kernel/cooking.ml OCAMLOPT kernel/term_typing.ml OCAMLOPT kernel/subtyping.ml OCAMLOPT kernel/mod_typing.ml OCAMLOPT kernel/safe_typing.ml OCAMLC kernel/vm.mli OCAMLOPT kernel/vm.ml OCAMLC kernel/csymtable.mli OCAMLOPT kernel/csymtable.ml OCAMLC kernel/vconv.mli OCAMLOPT kernel/vconv.ml OCAMLOPT -a -o kernel/kernel.cmxa OCAMLOPT library/nameops.ml OCAMLOPT library/libnames.ml OCAMLOPT library/libobject.ml OCAMLOPT library/summary.ml OCAMLOPT library/nametab.ml OCAMLOPT library/global.ml OCAMLOPT library/lib.ml OCAMLOPT pretyping/termops.ml OCAMLOPT pretyping/evd.ml OCAMLOPT pretyping/rawterm.ml OCAMLOPT pretyping/namegen.ml OCAMLOPT pretyping/reductionops.ml OCAMLOPT pretyping/inductiveops.ml OCAMLOPT library/goptions.ml OCAMLOPT pretyping/detyping.ml OCAMLOPT interp/topconstr.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/decls.mli OCAMLOPT library/decls.ml OCAMLC library/heads.mli OCAMLOPT library/heads.ml OCAMLC library/assumptions.mli OCAMLOPT library/assumptions.ml OCAMLOPT -a -o library/library.cmxa OCAMLC pretyping/vnorm.mli OCAMLOPT pretyping/vnorm.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/evarutil.mli OCAMLOPT pretyping/evarutil.ml OCAMLC pretyping/term_dnet.mli OCAMLOPT pretyping/term_dnet.ml OCAMLC pretyping/recordops.mli OCAMLOPT pretyping/recordops.ml OCAMLC pretyping/evarconv.mli OCAMLOPT pretyping/evarconv.ml OCAMLC pretyping/typing.mli OCAMLOPT pretyping/typing.ml OCAMLOPT pretyping/pattern.ml OCAMLC pretyping/matching.mli OCAMLOPT pretyping/matching.ml OCAMLC pretyping/tacred.mli OCAMLOPT pretyping/tacred.ml OCAMLC pretyping/typeclasses_errors.mli OCAMLOPT pretyping/typeclasses_errors.ml OCAMLC pretyping/typeclasses.mli OCAMLOPT pretyping/typeclasses.ml OCAMLOPT pretyping/classops.ml OCAMLC pretyping/coercion.mli OCAMLOPT pretyping/coercion.ml OCAMLC pretyping/unification.mli OCAMLOPT pretyping/unification.ml OCAMLC pretyping/clenv.mli OCAMLOPT pretyping/clenv.ml OCAMLC pretyping/indrec.mli OCAMLOPT pretyping/indrec.ml OCAMLC pretyping/cases.mli OCAMLOPT pretyping/cases.ml OCAMLC pretyping/pretyping.mli OCAMLOPT pretyping/pretyping.ml OCAMLOPT -a -o pretyping/pretyping.cmxa OCAMLOPT4 parsing/lexer.ml4 OCAMLOPT interp/ppextend.ml OCAMLOPT interp/notation.ml OCAMLC interp/dumpglob.mli OCAMLOPT interp/dumpglob.ml OCAMLOPT interp/genarg.ml OCAMLC interp/syntax_def.mli OCAMLOPT interp/syntax_def.ml OCAMLC interp/smartlocate.mli OCAMLOPT interp/smartlocate.ml OCAMLC interp/reserve.mli OCAMLOPT interp/reserve.ml OCAMLC library/impargs.mli OCAMLOPT library/impargs.ml OCAMLC interp/implicit_quantifiers.mli OCAMLOPT interp/implicit_quantifiers.ml 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 toplevel/discharge.mli OCAMLOPT toplevel/discharge.ml OCAMLC library/declare.mli OCAMLOPT library/declare.ml OCAMLOPT -a -o interp/interp.cmxa OCAMLOPT proofs/tacexpr.ml OCAMLC proofs/proof_type.mli OCAMLOPT proofs/proof_type.ml OCAMLC proofs/redexpr.mli OCAMLOPT proofs/redexpr.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/pfedit.mli OCAMLOPT proofs/pfedit.ml OCAMLC proofs/tactic_debug.mli OCAMLOPT proofs/tactic_debug.ml OCAMLC proofs/clenvtac.mli OCAMLOPT proofs/clenvtac.ml OCAMLC proofs/decl_mode.mli OCAMLOPT proofs/decl_mode.ml OCAMLOPT -a -o proofs/proofs.cmxa OCAMLOPT parsing/extend.ml OCAMLOPT parsing/extrawit.ml OCAMLOPT4 parsing/pcoq.ml4 OCAMLOPT toplevel/vernacexpr.ml OCAMLOPT parsing/egrammar.ml OCAMLOPT4 parsing/g_xml.ml4 OCAMLC parsing/ppconstr.mli OCAMLOPT parsing/ppconstr.ml OCAMLC parsing/printer.mli OCAMLOPT parsing/printer.ml OCAMLC parsing/pptactic.mli OCAMLOPT parsing/pptactic.ml OCAMLC parsing/ppdecl_proof.mli OCAMLOPT parsing/ppdecl_proof.ml OCAMLC parsing/tactic_printer.mli OCAMLOPT parsing/tactic_printer.ml OCAMLC parsing/printmod.mli OCAMLOPT parsing/printmod.ml OCAMLC parsing/prettyp.mli OCAMLOPT parsing/prettyp.ml OCAMLOPT -a -o parsing/parsing.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 OCAMLOPT4 tactics/hipattern.ml4 OCAMLC toplevel/ind_tables.mli OCAMLOPT toplevel/ind_tables.ml OCAMLC tactics/eqschemes.mli OCAMLOPT tactics/eqschemes.ml OCAMLC tactics/elimschemes.mli OCAMLOPT tactics/elimschemes.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/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 OCAMLC tactics/evar_tactics.mli OCAMLOPT tactics/evar_tactics.ml OCAMLC toplevel/himsg.mli OCAMLOPT toplevel/himsg.ml OCAMLC toplevel/vernacinterp.mli OCAMLOPT toplevel/vernacinterp.ml OCAMLC tactics/autorewrite.mli OCAMLOPT tactics/autorewrite.ml OCAMLC tactics/decl_interp.mli OCAMLOPT tactics/decl_interp.ml OCAMLC tactics/decl_proof_instr.mli OCAMLOPT tactics/decl_proof_instr.ml OCAMLC tactics/tactic_option.mli OCAMLOPT tactics/tactic_option.ml OCAMLOPT -a -o tactics/tactics.cmxa 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/auto_ind_decl.mli OCAMLOPT toplevel/auto_ind_decl.ml OCAMLC toplevel/libtypes.mli OCAMLOPT toplevel/libtypes.ml OCAMLC toplevel/search.mli OCAMLOPT toplevel/search.ml OCAMLC toplevel/autoinstance.mli OCAMLOPT toplevel/autoinstance.ml OCAMLC toplevel/lemmas.mli OCAMLOPT toplevel/lemmas.ml OCAMLC toplevel/indschemes.mli OCAMLOPT toplevel/indschemes.ml OCAMLC toplevel/command.mli OCAMLOPT toplevel/command.ml OCAMLC toplevel/classes.mli OCAMLOPT toplevel/classes.ml OCAMLC toplevel/record.mli OCAMLOPT toplevel/record.ml OCAMLC parsing/ppvernac.mli OCAMLOPT parsing/ppvernac.ml CAMLP4O toplevel/mltop.ml4 OCAMLC toplevel/mltop.mli OCAMLOPT toplevel/mltop.optml OCAMLC toplevel/vernacentries.mli OCAMLOPT toplevel/vernacentries.ml OCAMLC toplevel/whelp.mli OCAMLOPT4 toplevel/whelp.ml4 OCAMLC toplevel/vernac.mli OCAMLOPT toplevel/vernac.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_constr.ml4 OCAMLOPT4 parsing/g_vernac.ml4 OCAMLOPT4 parsing/g_prim.ml4 OCAMLOPT4 parsing/g_proofs.ml4 OCAMLOPT4 parsing/g_tactic.ml4 OCAMLOPT4 parsing/g_ltac.ml4 OCAMLOPT4 parsing/g_decl_mode.ml4 OCAMLOPT -a -o parsing/highparsing.cmxa OCAMLC tactics/refine.mli OCAMLOPT tactics/refine.ml OCAMLC tactics/extraargs.mli OCAMLOPT4 tactics/extraargs.ml4 OCAMLC tactics/extratactics.mli OCAMLOPT4 tactics/extratactics.ml4 OCAMLC tactics/eauto.mli OCAMLOPT4 tactics/eauto.ml4 OCAMLOPT4 tactics/class_tactics.ml4 OCAMLOPT4 tactics/rewrite.ml4 OCAMLOPT4 tactics/tauto.ml4 OCAMLOPT4 tactics/eqdecide.ml4 OCAMLOPT -a -o tactics/hightactics.cmxa OCAMLC kernel/byterun/coq_fix_code.c OCAMLC kernel/byterun/coq_memory.c OCAMLC kernel/byterun/coq_values.c OCAMLC kernel/byterun/coq_interp.c cd kernel/byterun/ && \ "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o "ranlib" kernel/byterun/libcoqrun.a COQMKTOP -o bin/coqtop.opt strip bin/coqtop.opt cd bin; ln -sf coqtop.opt coqtop COQC -nois theories/Init/Notations.v COQC -nois theories/Init/Logic.v Defining 'IF' as keyword Defining 'exists2' as keyword OCAMLC plugins/syntax/nat_syntax.ml OCAMLC plugins/syntax/nat_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/nat_syntax_plugin.cma OCAMLOPT plugins/syntax/nat_syntax.ml OCAMLOPT plugins/syntax/nat_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/nat_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs COQC -nois theories/Init/Datatypes.v COQC -nois theories/Init/Logic_Type.v COQC -nois theories/Init/Peano.v COQC -nois theories/Init/Specif.v COQC -nois theories/Init/Wf.v COQC -nois theories/Init/Tactics.v OCAMLC plugins/extraction/miniml.mli OCAMLC plugins/extraction/table.mli OCAMLC plugins/extraction/table.ml OCAMLC plugins/extraction/mlutil.mli OCAMLC plugins/extraction/mlutil.ml OCAMLC plugins/extraction/modutil.mli OCAMLC plugins/extraction/modutil.ml OCAMLC plugins/extraction/extraction.mli OCAMLC plugins/extraction/extraction.ml OCAMLC plugins/extraction/common.mli OCAMLC plugins/extraction/common.ml OCAMLC plugins/extraction/ocaml.mli OCAMLC plugins/extraction/ocaml.ml OCAMLC plugins/extraction/haskell.mli OCAMLC plugins/extraction/haskell.ml OCAMLC plugins/extraction/scheme.mli OCAMLC plugins/extraction/scheme.ml OCAMLC plugins/extraction/extract_env.mli OCAMLC plugins/extraction/extract_env.ml OCAMLC4 plugins/extraction/g_extraction.ml4 OCAMLC plugins/extraction/extraction_plugin_mod.ml OCAMLC -a -o plugins/extraction/extraction_plugin.cma OCAMLOPT plugins/extraction/table.ml OCAMLOPT plugins/extraction/mlutil.ml OCAMLOPT plugins/extraction/modutil.ml OCAMLOPT plugins/extraction/extraction.ml OCAMLOPT plugins/extraction/common.ml OCAMLOPT plugins/extraction/ocaml.ml OCAMLOPT plugins/extraction/haskell.ml OCAMLOPT plugins/extraction/scheme.ml OCAMLOPT plugins/extraction/extract_env.ml OCAMLOPT4 plugins/extraction/g_extraction.ml4 OCAMLOPT plugins/extraction/extraction_plugin_mod.ml OCAMLOPT -a -o plugins/extraction/extraction_plugin.cmxa OCAMLOPT -shared -o plugins/extraction/extraction_plugin.cmxs OCAMLC plugins/cc/ccalgo.mli OCAMLC plugins/cc/ccalgo.ml OCAMLC plugins/cc/ccproof.mli OCAMLC plugins/cc/ccproof.ml OCAMLC plugins/cc/cctac.mli OCAMLC plugins/cc/cctac.ml OCAMLC4 plugins/cc/g_congruence.ml4 OCAMLC plugins/cc/cc_plugin_mod.ml OCAMLC -a -o plugins/cc/cc_plugin.cma OCAMLOPT plugins/cc/ccalgo.ml OCAMLOPT plugins/cc/ccproof.ml OCAMLOPT plugins/cc/cctac.ml OCAMLOPT4 plugins/cc/g_congruence.ml4 OCAMLOPT plugins/cc/cc_plugin_mod.ml OCAMLOPT -a -o plugins/cc/cc_plugin.cmxa OCAMLOPT -shared -o plugins/cc/cc_plugin.cmxs OCAMLC plugins/firstorder/formula.mli OCAMLC plugins/firstorder/formula.ml OCAMLC plugins/firstorder/unify.mli OCAMLC plugins/firstorder/unify.ml OCAMLC plugins/firstorder/sequent.mli OCAMLC plugins/firstorder/sequent.ml OCAMLC plugins/firstorder/rules.mli OCAMLC plugins/firstorder/rules.ml OCAMLC plugins/firstorder/instances.mli OCAMLC plugins/firstorder/instances.ml OCAMLC plugins/firstorder/ground.mli OCAMLC plugins/firstorder/ground.ml OCAMLC4 plugins/firstorder/g_ground.ml4 OCAMLC plugins/firstorder/ground_plugin_mod.ml OCAMLC -a -o plugins/firstorder/ground_plugin.cma OCAMLOPT plugins/firstorder/formula.ml OCAMLOPT plugins/firstorder/unify.ml OCAMLOPT plugins/firstorder/sequent.ml OCAMLOPT plugins/firstorder/rules.ml OCAMLOPT plugins/firstorder/instances.ml OCAMLOPT plugins/firstorder/ground.ml OCAMLOPT4 plugins/firstorder/g_ground.ml4 OCAMLOPT plugins/firstorder/ground_plugin_mod.ml OCAMLOPT -a -o plugins/firstorder/ground_plugin.cmxa OCAMLOPT -shared -o plugins/firstorder/ground_plugin.cmxs OCAMLC plugins/dp/fol.mli OCAMLC plugins/dp/dp_why.mli OCAMLC plugins/dp/dp_why.ml OCAMLC plugins/dp/dp_zenon.mli OCAMLC plugins/dp/dp_zenon.ml OCAMLC plugins/dp/dp.mli OCAMLC plugins/dp/dp.ml OCAMLC4 plugins/dp/g_dp.ml4 OCAMLC plugins/dp/dp_plugin_mod.ml OCAMLC -a -o plugins/dp/dp_plugin.cma OCAMLOPT plugins/dp/dp_why.ml OCAMLOPT plugins/dp/dp_zenon.ml OCAMLOPT plugins/dp/dp.ml OCAMLOPT4 plugins/dp/g_dp.ml4 OCAMLOPT plugins/dp/dp_plugin_mod.ml OCAMLOPT -a -o plugins/dp/dp_plugin.cmxa OCAMLOPT -shared -o plugins/dp/dp_plugin.cmxs OCAMLC plugins/funind/indfun_common.mli OCAMLC plugins/funind/indfun_common.ml OCAMLC plugins/funind/rawtermops.mli OCAMLC plugins/funind/rawtermops.ml OCAMLC plugins/funind/recdef.ml OCAMLC plugins/funind/rawterm_to_relation.mli OCAMLC plugins/funind/rawterm_to_relation.ml OCAMLC plugins/funind/functional_principles_proofs.mli OCAMLC plugins/funind/functional_principles_proofs.ml OCAMLC plugins/funind/functional_principles_types.mli OCAMLC plugins/funind/functional_principles_types.ml OCAMLC4 tactics/tauto.ml4 OCAMLC plugins/funind/invfun.ml OCAMLC plugins/funind/indfun.ml OCAMLC plugins/funind/merge.ml OCAMLC4 plugins/funind/g_indfun.ml4 OCAMLC plugins/funind/recdef_plugin_mod.ml OCAMLC -a -o plugins/funind/recdef_plugin.cma OCAMLOPT plugins/funind/indfun_common.ml OCAMLOPT plugins/funind/rawtermops.ml OCAMLOPT plugins/funind/recdef.ml OCAMLOPT plugins/funind/rawterm_to_relation.ml OCAMLOPT plugins/funind/functional_principles_proofs.ml OCAMLOPT plugins/funind/functional_principles_types.ml OCAMLOPT plugins/funind/invfun.ml OCAMLOPT plugins/funind/indfun.ml OCAMLOPT plugins/funind/merge.ml OCAMLOPT4 plugins/funind/g_indfun.ml4 OCAMLOPT plugins/funind/recdef_plugin_mod.ml OCAMLOPT -a -o plugins/funind/recdef_plugin.cmxa OCAMLOPT -shared -o plugins/funind/recdef_plugin.cmxs OCAMLC plugins/subtac/subtac_utils.mli OCAMLC plugins/subtac/subtac_utils.ml OCAMLC plugins/subtac/eterm.mli OCAMLC plugins/subtac/eterm.ml OCAMLC plugins/subtac/subtac_errors.mli OCAMLC plugins/subtac/subtac_errors.ml OCAMLC plugins/subtac/subtac_coercion.mli OCAMLC plugins/subtac/subtac_coercion.ml OCAMLC plugins/subtac/subtac_obligations.mli OCAMLC plugins/subtac/subtac_obligations.ml OCAMLC plugins/subtac/subtac_cases.mli OCAMLC plugins/subtac/subtac_cases.ml OCAMLC plugins/subtac/subtac_pretyping_F.ml OCAMLC plugins/subtac/subtac_pretyping.mli OCAMLC plugins/subtac/subtac_pretyping.ml OCAMLC plugins/subtac/subtac_command.mli OCAMLC plugins/subtac/subtac_command.ml OCAMLC plugins/subtac/subtac_classes.mli OCAMLC plugins/subtac/subtac_classes.ml OCAMLC plugins/subtac/subtac.mli OCAMLC plugins/subtac/subtac.ml OCAMLC4 plugins/subtac/g_subtac.ml4 OCAMLC plugins/subtac/subtac_plugin_mod.ml OCAMLC -a -o plugins/subtac/subtac_plugin.cma OCAMLOPT plugins/subtac/subtac_utils.ml OCAMLOPT plugins/subtac/eterm.ml OCAMLOPT plugins/subtac/subtac_errors.ml OCAMLOPT plugins/subtac/subtac_coercion.ml OCAMLOPT plugins/subtac/subtac_obligations.ml OCAMLOPT plugins/subtac/subtac_cases.ml OCAMLOPT plugins/subtac/subtac_pretyping_F.ml OCAMLOPT plugins/subtac/subtac_pretyping.ml OCAMLOPT plugins/subtac/subtac_command.ml OCAMLOPT plugins/subtac/subtac_classes.ml OCAMLOPT plugins/subtac/subtac.ml OCAMLOPT4 plugins/subtac/g_subtac.ml4 OCAMLOPT plugins/subtac/subtac_plugin_mod.ml OCAMLOPT -a -o plugins/subtac/subtac_plugin.cmxa OCAMLOPT -shared -o plugins/subtac/subtac_plugin.cmxs OCAMLC plugins/xml/unshare.mli OCAMLC plugins/xml/unshare.ml OCAMLC plugins/xml/xml.mli OCAMLC4 plugins/xml/xml.ml4 OCAMLC plugins/xml/acic.ml OCAMLC plugins/xml/doubleTypeInference.mli OCAMLC plugins/xml/doubleTypeInference.ml OCAMLC plugins/xml/cic2acic.ml OCAMLC4 plugins/xml/acic2Xml.ml4 OCAMLC plugins/xml/proof2aproof.ml OCAMLC plugins/xml/xmlcommand.mli OCAMLC plugins/xml/xmlcommand.ml OCAMLC4 plugins/xml/proofTree2Xml.ml4 OCAMLC4 plugins/xml/xmlentries.ml4 OCAMLC plugins/xml/cic2Xml.ml OCAMLC4 plugins/xml/dumptree.ml4 OCAMLC plugins/xml/xml_plugin_mod.ml OCAMLC -a -o plugins/xml/xml_plugin.cma OCAMLOPT plugins/xml/unshare.ml OCAMLOPT4 plugins/xml/xml.ml4 OCAMLOPT plugins/xml/acic.ml OCAMLOPT plugins/xml/doubleTypeInference.ml OCAMLOPT plugins/xml/cic2acic.ml OCAMLOPT4 plugins/xml/acic2Xml.ml4 OCAMLOPT plugins/xml/proof2aproof.ml OCAMLOPT plugins/xml/xmlcommand.ml OCAMLOPT4 plugins/xml/proofTree2Xml.ml4 OCAMLOPT4 plugins/xml/xmlentries.ml4 OCAMLOPT plugins/xml/cic2Xml.ml OCAMLOPT4 plugins/xml/dumptree.ml4 OCAMLOPT plugins/xml/xml_plugin_mod.ml OCAMLOPT -a -o plugins/xml/xml_plugin.cmxa OCAMLOPT -shared -o plugins/xml/xml_plugin.cmxs COQC -nois theories/Init/Prelude.v COQDEP states/MakeInitial.v BUILD states/initial.coq OCAMLC plugins/syntax/z_syntax.ml OCAMLC plugins/syntax/z_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/z_syntax_plugin.cma OCAMLOPT plugins/syntax/z_syntax.ml OCAMLOPT plugins/syntax/z_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/z_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/z_syntax_plugin.cmxs COQC theories/Logic/EqdepFacts.v COQC theories/Logic/Eqdep_dec.v COQC theories/NArith/BinPos.v COQC theories/NArith/BinNat.v COQC theories/Arith/Le.v COQC theories/Arith/Lt.v COQC theories/Arith/Plus.v COQC theories/Arith/Gt.v COQC theories/Arith/Minus.v COQC theories/Arith/Mult.v COQC theories/Logic/Decidable.v COQC theories/Arith/Compare_dec.v COQC theories/NArith/Pnat.v COQC theories/ZArith/BinInt.v COQC theories/ZArith/Zcompare.v COQC theories/Arith/Between.v COQC theories/Arith/Peano_dec.v COQC theories/Arith/Factorial.v COQC theories/Arith/EqNat.v COQC theories/Arith/Wf_nat.v COQC theories/Arith/Arith_base.v COQC theories/ZArith/Zorder.v COQC theories/ZArith/Zeven.v COQC theories/Relations/Relation_Definitions.v COQC theories/Relations/Relation_Operators.v COQC theories/Relations/Operators_Properties.v COQC theories/Relations/Relations.v COQC theories/Program/Basics.v COQC theories/Program/Tactics.v COQC theories/Classes/Init.v COQC theories/Classes/RelationClasses.v COQC theories/Classes/Morphisms.v COQC theories/Classes/Morphisms_Prop.v COQC theories/Classes/Equivalence.v COQC theories/Classes/SetoidTactics.v COQC theories/Setoids/Setoid.v COQC theories/Structures/Equalities.v COQC theories/Structures/Orders.v COQC theories/Bool/Sumbool.v COQC theories/ZArith/ZArith_dec.v COQC theories/ZArith/Zbool.v COQC theories/Structures/OrdersTac.v COQC theories/ZArith/ZOrderedType.v COQC theories/Structures/OrdersFacts.v COQC theories/Structures/GenericMinMax.v COQC theories/ZArith/Zminmax.v COQC theories/ZArith/Zmin.v COQC theories/ZArith/Zmax.v COQC theories/Arith/NatOrderedType.v COQC theories/Arith/MinMax.v COQC theories/Arith/Min.v COQC theories/Arith/Max.v COQC theories/ZArith/Znat.v COQC theories/ZArith/Zabs.v COQC theories/ZArith/auxiliary.v COQC theories/Bool/Bool.v COQC theories/ZArith/Zmisc.v COQC theories/ZArith/Wf_Z.v COQC theories/ZArith/Zhints.v COQC theories/ZArith/ZArith_base.v COQC plugins/omega/OmegaLemmas.v OCAMLC plugins/omega/omega.ml OCAMLC plugins/omega/coq_omega.ml OCAMLC4 plugins/omega/g_omega.ml4 OCAMLC plugins/omega/omega_plugin_mod.ml OCAMLC -a -o plugins/omega/omega_plugin.cma OCAMLOPT plugins/omega/omega.ml OCAMLOPT plugins/omega/coq_omega.ml OCAMLOPT4 plugins/omega/g_omega.ml4 OCAMLOPT plugins/omega/omega_plugin_mod.ml OCAMLOPT -a -o plugins/omega/omega_plugin.cmxa OCAMLOPT -shared -o plugins/omega/omega_plugin.cmxs COQC plugins/omega/OmegaPlugin.v COQC theories/Arith/Even.v COQC theories/Arith/Div2.v COQC theories/NArith/Nnat.v COQC plugins/setoid_ring/Ring_theory.v OCAMLC plugins/quote/quote.ml OCAMLC4 plugins/quote/g_quote.ml4 OCAMLC plugins/quote/quote_plugin_mod.ml OCAMLC -a -o plugins/quote/quote_plugin.cma OCAMLOPT plugins/quote/quote.ml OCAMLOPT4 plugins/quote/g_quote.ml4 OCAMLOPT plugins/quote/quote_plugin_mod.ml OCAMLOPT -a -o plugins/quote/quote_plugin.cmxa OCAMLOPT -shared -o plugins/quote/quote_plugin.cmxs COQC plugins/quote/Quote.v OCAMLC4 tactics/class_tactics.ml4 OCAMLC4 tactics/rewrite.ml4 OCAMLC4 plugins/setoid_ring/newring.ml4 OCAMLC plugins/setoid_ring/newring_plugin_mod.ml OCAMLC -a -o plugins/setoid_ring/newring_plugin.cma OCAMLOPT4 plugins/setoid_ring/newring.ml4 OCAMLOPT plugins/setoid_ring/newring_plugin_mod.ml OCAMLOPT -a -o plugins/setoid_ring/newring_plugin.cmxa OCAMLOPT -shared -o plugins/setoid_ring/newring_plugin.cmxs COQC theories/Lists/List.v COQC theories/Lists/ListTactics.v COQC plugins/setoid_ring/BinList.v COQC plugins/setoid_ring/Ring_polynom.v COQC theories/ZArith/Zpow_def.v COQC theories/ZArith/ZOdiv_def.v COQC plugins/setoid_ring/InitialRing.v COQC plugins/setoid_ring/Ring_tac.v COQC plugins/setoid_ring/Ring_base.v COQC plugins/setoid_ring/Ring.v COQC plugins/setoid_ring/ArithRing.v COQC theories/Arith/Arith.v COQC theories/Bool/Bvector.v COQC theories/NArith/Ndigits.v COQC plugins/setoid_ring/NArithRing.v COQC theories/NArith/NArith.v COQC plugins/omega/PreOmega.v COQC plugins/omega/Omega.v COQC plugins/romega/ReflOmegaCore.v OCAMLC plugins/romega/const_omega.mli OCAMLC plugins/romega/const_omega.ml OCAMLC plugins/romega/refl_omega.ml OCAMLC4 plugins/romega/g_romega.ml4 OCAMLC plugins/romega/romega_plugin_mod.ml OCAMLC -a -o plugins/romega/romega_plugin.cma OCAMLOPT plugins/romega/const_omega.ml OCAMLOPT plugins/romega/refl_omega.ml OCAMLOPT4 plugins/romega/g_romega.ml4 OCAMLOPT plugins/romega/romega_plugin_mod.ml OCAMLOPT -a -o plugins/romega/romega_plugin.cmxa OCAMLOPT -shared -o plugins/romega/romega_plugin.cmxs COQC plugins/romega/ROmega.v COQC plugins/micromega/Refl.v COQC plugins/micromega/CheckerMaker.v COQC plugins/setoid_ring/ZArithRing.v COQC theories/ZArith/Zcomplements.v COQC theories/ZArith/Zsqrt.v COQC theories/ZArith/Zpower.v COQC theories/ZArith/Zdiv.v Defining 'mod' as keyword COQC theories/ZArith/Zlogarithm.v COQC theories/ZArith/ZArith.v COQC plugins/micromega/Env.v COQC plugins/micromega/EnvRing.v COQC plugins/micromega/OrderedRing.v COQC plugins/micromega/Tauto.v COQC plugins/micromega/RingMicromega.v COQC plugins/micromega/ZCoeff.v COQC theories/QArith/QArith_base.v COQC plugins/setoid_ring/Field_theory.v COQC plugins/setoid_ring/Field_tac.v COQC plugins/setoid_ring/Field.v COQC theories/QArith/Qfield.v COQC theories/QArith/Qring.v COQC theories/ZArith/Znumtheory.v COQC theories/QArith/Qreduction.v COQC theories/QArith/QArith.v COQC plugins/micromega/VarMap.v COQC plugins/micromega/ZMicromega.v COQC plugins/micromega/QMicromega.v OCAMLC plugins/syntax/r_syntax.ml OCAMLC plugins/syntax/r_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/r_syntax_plugin.cma OCAMLOPT plugins/syntax/r_syntax.ml OCAMLOPT plugins/syntax/r_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/r_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/r_syntax_plugin.cmxs COQC theories/Reals/Rdefinitions.v COQC theories/Reals/Raxioms.v COQC theories/Reals/Rpow_def.v COQC plugins/setoid_ring/RealField.v COQC theories/Reals/RIneq.v COQC theories/Reals/DiscrR.v COQC plugins/micromega/RMicromega.v COQC plugins/ring/LegacyRing_theory.v COQC plugins/ring/Ring_normalize.v OCAMLC plugins/micromega/sos_types.ml OCAMLC plugins/micromega/micromega.mli OCAMLC plugins/micromega/mutils.ml OCAMLC plugins/micromega/micromega.ml OCAMLC plugins/micromega/mfourier.ml OCAMLC plugins/micromega/sos_lib.ml OCAMLC plugins/fourier/fourier.ml OCAMLC plugins/micromega/certificate.ml OCAMLC plugins/micromega/persistent_cache.ml OCAMLC plugins/micromega/coq_micromega.ml OCAMLC plugins/ring/ring.ml OCAMLC4 plugins/micromega/g_micromega.ml4 OCAMLC plugins/micromega/micromega_plugin_mod.ml OCAMLC -a -o plugins/micromega/micromega_plugin.cma OCAMLOPT plugins/micromega/sos_types.ml OCAMLOPT plugins/micromega/micromega.ml OCAMLOPT plugins/micromega/mutils.ml OCAMLOPT plugins/micromega/mfourier.ml OCAMLOPT plugins/micromega/sos_lib.ml OCAMLOPT plugins/fourier/fourier.ml OCAMLOPT plugins/micromega/certificate.ml OCAMLOPT plugins/micromega/persistent_cache.ml OCAMLOPT plugins/micromega/coq_micromega.ml OCAMLOPT plugins/ring/ring.ml OCAMLOPT4 plugins/micromega/g_micromega.ml4 OCAMLOPT plugins/micromega/micromega_plugin_mod.ml OCAMLOPT -a -o plugins/micromega/micromega_plugin.cmxa OCAMLOPT -shared -o plugins/micromega/micromega_plugin.cmxs COQC plugins/micromega/Psatz.v COQC plugins/ring/Ring_abstract.v OCAMLC4 plugins/ring/g_ring.ml4 OCAMLC plugins/ring/ring_plugin_mod.ml OCAMLC -a -o plugins/ring/ring_plugin.cma OCAMLOPT4 plugins/ring/g_ring.ml4 OCAMLOPT plugins/ring/ring_plugin_mod.ml OCAMLOPT -a -o plugins/ring/ring_plugin.cmxa OCAMLOPT -shared -o plugins/ring/ring_plugin.cmxs COQC plugins/ring/LegacyRing.v COQC plugins/ring/LegacyArithRing.v COQC plugins/ring/LegacyNArithRing.v COQC plugins/ring/LegacyZArithRing.v COQC plugins/ring/Setoid_ring_theory.v COQC plugins/ring/Setoid_ring_normalize.v COQC plugins/ring/Setoid_ring.v COQC plugins/field/LegacyField_Compl.v COQC plugins/field/LegacyField_Theory.v COQC plugins/field/LegacyField_Tactic.v OCAMLC4 plugins/field/field.ml4 OCAMLC plugins/field/field_plugin_mod.ml OCAMLC -a -o plugins/field/field_plugin.cma OCAMLOPT4 plugins/field/field.ml4 OCAMLOPT plugins/field/field_plugin_mod.ml OCAMLOPT -a -o plugins/field/field_plugin.cmxa OCAMLOPT -shared -o plugins/field/field_plugin.cmxs COQC plugins/field/LegacyField.v COQC theories/Reals/Rbase.v COQC plugins/fourier/Fourier_util.v OCAMLC plugins/fourier/fourierR.ml OCAMLC4 plugins/fourier/g_fourier.ml4 OCAMLC plugins/fourier/fourier_plugin_mod.ml OCAMLC -a -o plugins/fourier/fourier_plugin.cma OCAMLOPT plugins/fourier/fourierR.ml OCAMLOPT4 plugins/fourier/g_fourier.ml4 OCAMLOPT plugins/fourier/fourier_plugin_mod.ml OCAMLOPT -a -o plugins/fourier/fourier_plugin.cmxa OCAMLOPT -shared -o plugins/fourier/fourier_plugin.cmxs COQC plugins/fourier/Fourier.v COQC plugins/funind/Recdef.v COQC plugins/rtauto/Bintree.v OCAMLC plugins/rtauto/proof_search.mli OCAMLC plugins/rtauto/proof_search.ml OCAMLC plugins/rtauto/refl_tauto.mli OCAMLC plugins/rtauto/refl_tauto.ml OCAMLC4 plugins/rtauto/g_rtauto.ml4 OCAMLC plugins/rtauto/rtauto_plugin_mod.ml OCAMLC -a -o plugins/rtauto/rtauto_plugin.cma OCAMLOPT plugins/rtauto/proof_search.ml OCAMLOPT plugins/rtauto/refl_tauto.ml OCAMLOPT4 plugins/rtauto/g_rtauto.ml4 OCAMLOPT plugins/rtauto/rtauto_plugin_mod.ml OCAMLOPT -a -o plugins/rtauto/rtauto_plugin.cmxa OCAMLOPT -shared -o plugins/rtauto/rtauto_plugin.cmxs COQC plugins/rtauto/Rtauto.v COQC plugins/setoid_ring/Ring_equiv.v COQC theories/Logic/Hurkens.v COQC theories/Logic/ClassicalFacts.v COQC theories/Logic/Classical_Prop.v COQC theories/Logic/Classical_Pred_Type.v COQC theories/Logic/Classical.v COQC plugins/dp/Dp.v OCAMLC plugins/nsatz/utile.mli OCAMLC plugins/nsatz/utile.ml OCAMLC plugins/nsatz/polynom.mli OCAMLC plugins/nsatz/polynom.ml OCAMLC plugins/nsatz/ideal.ml OCAMLC4 plugins/nsatz/nsatz.ml4 OCAMLC plugins/nsatz/nsatz_plugin_mod.ml OCAMLC -a -o plugins/nsatz/nsatz_plugin.cma OCAMLOPT plugins/nsatz/utile.ml OCAMLOPT plugins/nsatz/polynom.ml OCAMLOPT plugins/nsatz/ideal.ml OCAMLOPT4 plugins/nsatz/nsatz.ml4 OCAMLOPT plugins/nsatz/nsatz_plugin_mod.ml OCAMLOPT -a -o plugins/nsatz/nsatz_plugin.cmxa OCAMLOPT -shared -o plugins/nsatz/nsatz_plugin.cmxs COQC theories/Reals/R_Ifp.v COQC theories/Reals/Rbasic_fun.v COQC theories/Reals/R_sqr.v COQC theories/Reals/SplitAbsolu.v COQC theories/Reals/SplitRmult.v COQC theories/Reals/ArithProp.v COQC theories/Reals/Rfunctions.v COQC theories/Arith/Compare.v COQC theories/Reals/Rseries.v COQC theories/Reals/SeqProp.v COQC theories/Reals/Rcomplete.v COQC theories/Reals/PartSum.v COQC theories/Reals/AltSeries.v COQC theories/Reals/Binomial.v COQC theories/Reals/Rsigma.v COQC theories/Reals/Rprod.v COQC theories/Reals/Cauchy_prod.v COQC theories/Reals/Alembert.v COQC theories/Reals/SeqSeries.v COQC theories/Reals/Rtrigo_fun.v COQC theories/Reals/Rtrigo_def.v COQC theories/Reals/Rtrigo_alt.v COQC theories/Reals/Cos_rel.v COQC theories/Reals/Cos_plus.v COQC theories/Reals/Rtrigo.v COQC theories/Reals/Rlimit.v COQC theories/Reals/Rderiv.v COQC theories/Reals/Ranalysis1.v Defining 'o' as keyword COQC theories/Reals/Ranalysis2.v COQC theories/Reals/Ranalysis3.v COQC theories/Reals/RList.v COQC theories/Reals/Rtopology.v COQC theories/Reals/MVT.v COQC theories/Reals/PSeries_reg.v COQC theories/Reals/Exp_prop.v COQC theories/Reals/Rtrigo_reg.v COQC theories/Reals/Rsqrt_def.v COQC theories/Reals/R_sqrt.v COQC theories/Reals/Rtrigo_calc.v COQC theories/Reals/Rgeom.v COQC theories/Reals/Sqrt_reg.v COQC theories/Reals/Ranalysis4.v COQC theories/Reals/Rpower.v COQC theories/Reals/Ranalysis.v COQC theories/Reals/NewtonInt.v COQC theories/Reals/RiemannInt_SF.v COQC theories/Reals/RiemannInt.v COQC theories/Reals/Integration.v COQC theories/Reals/Reals.v COQC plugins/nsatz/Nsatz.v COQC plugins/extraction/ExtrOcamlBasic.v COQC plugins/extraction/ExtrOcamlIntConv.v COQC plugins/extraction/ExtrOcamlBigIntConv.v COQC theories/Arith/Euclid.v COQC plugins/extraction/ExtrOcamlNatInt.v COQC plugins/extraction/ExtrOcamlNatBigInt.v COQC plugins/extraction/ExtrOcamlZInt.v COQC plugins/extraction/ExtrOcamlZBigInt.v OCAMLC plugins/syntax/ascii_syntax.ml OCAMLC plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/ascii_syntax_plugin.cma OCAMLOPT plugins/syntax/ascii_syntax.ml OCAMLOPT plugins/syntax/ascii_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/ascii_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/ascii_syntax_plugin.cmxs COQC theories/Strings/Ascii.v OCAMLC plugins/syntax/string_syntax.ml OCAMLC plugins/syntax/string_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/string_syntax_plugin.cma OCAMLOPT plugins/syntax/string_syntax.ml OCAMLOPT plugins/syntax/string_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/string_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/string_syntax_plugin.cmxs COQC theories/Strings/String.v COQC plugins/extraction/ExtrOcamlString.v COQC theories/Logic/Berardi.v COQC theories/Logic/ChoiceFacts.v COQC theories/Logic/ClassicalUniqueChoice.v COQC theories/Logic/RelationalChoice.v COQC theories/Logic/ClassicalChoice.v COQC theories/Logic/ClassicalDescription.v COQC theories/Logic/ClassicalEpsilon.v COQC theories/Logic/Classical_Pred_Set.v COQC theories/Logic/Classical_Type.v COQC theories/Logic/ConstructiveEpsilon.v COQC theories/Logic/Description.v COQC theories/Logic/Diaconescu.v COQC theories/Logic/Epsilon.v COQC theories/Logic/Eqdep.v COQC theories/Logic/FunctionalExtensionality.v COQC theories/Logic/IndefiniteDescription.v COQC theories/Logic/JMeq.v COQC theories/Logic/ProofIrrelevanceFacts.v COQC theories/Logic/ProofIrrelevance.v COQC theories/Logic/SetIsType.v COQC theories/Arith/Bool_nat.v COQC theories/Bool/BoolEq.v COQC theories/Bool/DecBool.v COQC theories/Bool/IfProp.v COQC theories/Bool/Zerob.v COQC theories/NArith/Ndec.v COQC theories/NArith/Ndist.v COQC theories/NArith/POrderedType.v COQC theories/NArith/Pminmax.v COQC theories/NArith/NOrderedType.v COQC theories/NArith/Nminmax.v COQC theories/ZArith/Int.v COQC theories/ZArith/Zdigits.v COQC theories/ZArith/Zgcd_alt.v COQC theories/ZArith/ZOdiv.v Defining 'mod' as keyword COQC theories/ZArith/Zpow_facts.v COQC theories/ZArith/Zwf.v COQC theories/Lists/ListSet.v COQC theories/Sets/Relations_1.v COQC theories/Sorting/Sorted.v COQC theories/Sorting/Permutation.v COQC theories/Sorting/Mergesort.v COQC theories/Sorting/Sorting.v COQC theories/Lists/SetoidList.v COQC theories/Lists/Streams.v COQC theories/Lists/StreamMemo.v COQC theories/Lists/TheoryList.v COQC theories/Sets/Ensembles.v COQC theories/Sets/Constructive_sets.v COQC theories/Sets/Classical_sets.v COQC theories/Sets/Partial_Order.v COQC theories/Sets/Cpo.v COQC theories/Sets/Finite_sets.v COQC theories/Sets/Relations_1_facts.v COQC theories/Sets/Powerset.v COQC theories/Sets/Powerset_facts.v COQC theories/Sets/Powerset_Classical_facts.v COQC theories/Sets/Finite_sets_facts.v COQC theories/Sets/Image.v COQC theories/Sets/Infinite_sets.v COQC theories/Sets/Integers.v COQC theories/Sets/Permut.v COQC theories/Sets/Multiset.v COQC theories/Sets/Relations_2.v COQC theories/Sets/Relations_2_facts.v COQC theories/Sets/Relations_3.v COQC theories/Sets/Relations_3_facts.v COQC theories/Sets/Uniset.v COQC theories/Structures/DecidableType.v COQC theories/Structures/OrderedType.v COQC theories/FSets/FMapInterface.v COQC theories/FSets/FMapList.v COQC theories/FSets/FMapAVL.v COQC theories/Structures/OrderedTypeEx.v COQC theories/Structures/DecidableTypeEx.v COQC theories/FSets/FMapFacts.v COQC theories/FSets/FMapFullAVL.v COQC theories/FSets/FMapPositive.v COQC theories/Structures/OrderedTypeAlt.v COQC theories/FSets/FMapWeakList.v COQC theories/FSets/FMaps.v COQC theories/FSets/FSetInterface.v COQC theories/FSets/FSetFacts.v COQC theories/Classes/RelationPairs.v COQC theories/MSets/MSetInterface.v COQC theories/MSets/MSetFacts.v COQC theories/FSets/FSetCompat.v COQC theories/MSets/MSetAVL.v COQC theories/Structures/OrdersAlt.v COQC theories/FSets/FSetAVL.v COQC theories/FSets/FSetPositive.v COQC theories/FSets/FSetBridge.v COQC theories/FSets/FSetDecide.v COQC theories/FSets/FSetProperties.v COQC theories/FSets/FSetEqProperties.v COQC theories/Structures/OrdersLists.v COQC theories/MSets/MSetList.v COQC theories/FSets/FSetList.v COQC theories/MSets/MSetWeakList.v COQC theories/FSets/FSetWeakList.v COQC theories/FSets/FSets.v COQC theories/FSets/FSetToFiniteSet.v COQC theories/MSets/MSetDecide.v COQC theories/MSets/MSetProperties.v COQC theories/MSets/MSetEqProperties.v COQC theories/Structures/EqualitiesFacts.v COQC theories/Structures/OrdersEx.v COQC theories/MSets/MSetPositive.v COQC theories/MSets/MSets.v COQC theories/MSets/MSetToFiniteSet.v COQC theories/Wellfounded/Disjoint_Union.v COQC theories/Wellfounded/Inclusion.v COQC theories/Wellfounded/Inverse_Image.v COQC theories/Wellfounded/Transitive_Closure.v COQC theories/Wellfounded/Lexicographic_Exponentiation.v COQC theories/Wellfounded/Lexicographic_Product.v COQC theories/Wellfounded/Union.v COQC theories/Wellfounded/Well_Ordering.v COQC theories/Wellfounded/Wellfounded.v COQC theories/Reals/LegacyRfield.v COQC theories/Reals/Rlogic.v COQC theories/Reals/ROrderedType.v COQC theories/Reals/Rminmax.v COQC theories/Sorting/PermutSetoid.v COQC theories/Sorting/Heap.v COQC theories/Sorting/PermutEq.v COQC theories/QArith/Qabs.v COQC theories/QArith/Qcanon.v COQC theories/QArith/Qpower.v COQC theories/QArith/Qreals.v COQC theories/QArith/Qround.v COQC theories/QArith/QOrderedType.v COQC theories/QArith/Qminmax.v OCAMLC plugins/syntax/numbers_syntax.ml OCAMLC plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLC -a -o plugins/syntax/numbers_syntax_plugin.cma OCAMLOPT plugins/syntax/numbers_syntax.ml OCAMLOPT plugins/syntax/numbers_syntax_plugin_mod.ml OCAMLOPT -a -o plugins/syntax/numbers_syntax_plugin.cmxa OCAMLOPT -shared -o plugins/syntax/numbers_syntax_plugin.cmxs COQC theories/Numbers/BigNumPrelude.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v COQC theories/Numbers/NumPrelude.v COQC theories/Numbers/NatInt/NZAxioms.v COQC theories/Numbers/Cyclic/Abstract/NZCyclic.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v COQC theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v COQC theories/Numbers/NaryFunctions.v COQC theories/Numbers/Cyclic/Int31/Int31.v COQC theories/Numbers/Cyclic/Int31/Cyclic31.v COQC theories/Numbers/Cyclic/Int31/Ring31.v COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v COQC theories/Numbers/Integer/Abstract/ZAxioms.v COQC theories/Numbers/NatInt/NZBase.v COQC theories/Numbers/NatInt/NZAdd.v COQC theories/Numbers/NatInt/NZMul.v COQC theories/Numbers/NatInt/NZOrder.v COQC theories/Numbers/NatInt/NZAddOrder.v COQC theories/Numbers/NatInt/NZMulOrder.v COQC theories/Numbers/NatInt/NZProperties.v COQC theories/Numbers/Integer/Abstract/ZBase.v COQC theories/Numbers/Integer/Abstract/ZAdd.v COQC theories/Numbers/Integer/Abstract/ZMul.v COQC theories/Numbers/Integer/Abstract/ZLt.v COQC theories/Numbers/Integer/Abstract/ZAddOrder.v COQC theories/Numbers/Integer/Abstract/ZMulOrder.v COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v COQC theories/Numbers/Integer/Abstract/ZProperties.v COQC theories/Numbers/NatInt/NZDiv.v Defining 'mod' as keyword COQC theories/Numbers/Integer/Abstract/ZDivFloor.v COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v COQC theories/Numbers/Integer/Abstract/ZDivEucl.v COQC theories/Numbers/Natural/SpecViaZ/NSig.v COQC theories/Numbers/Natural/Abstract/NAxioms.v COQC theories/Numbers/Natural/Abstract/NBase.v COQC theories/Numbers/Natural/Abstract/NAdd.v COQC theories/Numbers/Natural/Abstract/NOrder.v COQC theories/Numbers/Natural/Abstract/NAddOrder.v COQC theories/Numbers/Natural/Abstract/NMulOrder.v COQC theories/Numbers/Natural/Abstract/NSub.v COQC theories/Numbers/Natural/Abstract/NProperties.v COQC theories/Numbers/Natural/Abstract/NDiv.v COQC theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v COQC theories/Numbers/Natural/BigN/Nbasic.v COQC theories/Numbers/Natural/BigN/NMake_gen.v COQC theories/Numbers/Natural/BigN/NMake.v COQC theories/Numbers/Natural/BigN/BigN.v COQC theories/Numbers/Integer/SpecViaZ/ZSig.v COQC theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v COQC theories/Numbers/Integer/BigZ/ZMake.v COQC theories/Numbers/Integer/BigZ/BigZ.v COQC theories/Numbers/Integer/Binary/ZBinary.v COQC theories/Numbers/Integer/NatPairs/ZNatPairs.v COQC theories/Numbers/NatInt/NZDomain.v COQC theories/Numbers/Natural/Abstract/NStrongRec.v COQC theories/Numbers/Natural/Abstract/NDefOps.v COQC theories/Numbers/Natural/Abstract/NIso.v COQC theories/Numbers/Natural/Binary/NBinary.v COQC theories/Numbers/Natural/Peano/NPeano.v Defining 'mod' as keyword COQC theories/Numbers/Rational/SpecViaQ/QSig.v COQC theories/Numbers/Rational/BigQ/QMake.v COQC theories/Numbers/Rational/BigQ/BigQ.v COQC theories/Unicode/Utf8.v COQC theories/Unicode/Utf8_core.v COQC theories/Program/Utils.v COQC theories/Program/Wf.v COQC theories/Program/Equality.v COQC theories/Program/Subset.v COQC theories/Program/Combinators.v COQC theories/Program/Syntax.v COQC theories/Program/Program.v COQC theories/Classes/EquivDec.v COQC theories/Classes/Morphisms_Relations.v COQC theories/Classes/SetoidClass.v COQC theories/Classes/SetoidDec.v (cd `dirname doc/refman/RefMan-gal.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-gal.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-ext.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-ext.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-mod.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-mod.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-tac.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-tac.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-cic.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-cic.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-lib.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-lib.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-tacex.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-tacex.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-syn.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-syn.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-oth.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-oth.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-ltac.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-ltac.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/RefMan-decl.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/RefMan-decl.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Cases.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Cases.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Coercion.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Coercion.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Extraction.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Extraction.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Program.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Program.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Omega.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Omega.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Micromega.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Micromega.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Polynom.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Polynom.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Nsatz.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Nsatz.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Setoid.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Setoid.tex`) Your version of coqtop seems OK (cd `dirname doc/refman/Classes.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/refman/Classes.tex`) Your version of coqtop seems OK printf '\\newcommand{\\coqversion}{8.3pl4}' > doc/common/version.tex This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode (cd doc/refman; BIBINPUTS=.: hevea -fix -exec xxdate.exe ./styles.hva ./Reference-Manual.tex) Exclude comment 'comment' ./RefMan-int.tex:9: Warning: Undefined citation: 'CoqArt' ./RefMan-int.tex:50: Warning: Undefined label: 'Addoc-coqc' ./RefMan-int.tex:54: Warning: Undefined citation: 'ProofGeneral' ./RefMan-int.tex:55: Warning: Undefined citation: 'Pcoq' ./RefMan-int.tex:57: Warning: Undefined label: 'Addoc-coqide' ./RefMan-int.tex:67: Warning: Undefined label: 'Gallina' ./RefMan-int.tex:67: Warning: Undefined label: 'Gallina-extension' ./RefMan-int.tex:70: Warning: Undefined label: 'Theories' ./RefMan-int.tex:71: Warning: Undefined label: 'Cic' ./RefMan-int.tex:72: Warning: Undefined label: 'chapter:Modules' ./RefMan-int.tex:75: Warning: Undefined label: 'Vernacular-commands' ./RefMan-int.tex:80: Warning: Undefined label: 'Proof-handling' ./RefMan-int.tex:81: Warning: Undefined label: 'Tactics' ./RefMan-int.tex:84: Warning: Undefined label: 'TacticLanguage' ./RefMan-int.tex:85: Warning: Undefined label: 'Tactics-examples' ./RefMan-int.tex:93: Warning: Undefined label: 'Addoc-syntax' ./RefMan-int.tex:96: Warning: Undefined label: 'Addoc-coqc' ./RefMan-int.tex:98: Warning: Undefined label: 'Utilities' ./RefMan-int.tex:101: Warning: Undefined label: 'Addoc-coqide' ./RefMan-gal.v.tex:10: Warning: Undefined label: 'term' ./RefMan-gal.v.tex:12: Warning: Undefined label: 'Vernacular' ./RefMan-gal.v.tex:16: Warning: Undefined label: 'Cic' ./RefMan-gal.v.tex:220: Warning: Undefined label: 'term-syntax' ./RefMan-gal.v.tex:220: Warning: Undefined label: 'term-syntax-aux' ./RefMan-gal.v.tex:223: Warning: Undefined label: 'Cic' ./RefMan-gal.v.tex:224: Warning: Undefined label: 'Gallina-extension' ./RefMan-gal.v.tex:225: Warning: Undefined label: 'Addoc-syntax' ./RefMan-gal.v.tex:231: Warning: Undefined label: 'products' ./RefMan-gal.v.tex:232: Warning: Undefined label: 'abstractions' ./RefMan-gal.v.tex:233: Warning: Undefined label: 'fixpoints' ./RefMan-gal.v.tex:234: Warning: Undefined label: 'fixpoints' ./RefMan-gal.v.tex:236: Warning: Undefined label: 'let-in' ./RefMan-gal.v.tex:237: Warning: Undefined label: 'fixpoints' ./RefMan-gal.v.tex:239: Warning: Undefined label: 'fixpoints' ./RefMan-gal.v.tex:242: Warning: Undefined label: 'caseanalysis' ./RefMan-gal.v.tex:242: Warning: Undefined label: 'Mult-match' ./RefMan-gal.v.tex:244: Warning: Undefined label: 'caseanalysis' ./RefMan-gal.v.tex:244: Warning: Undefined label: 'Mult-match' ./RefMan-gal.v.tex:245: Warning: Undefined label: 'typecast' ./RefMan-gal.v.tex:246: Warning: Undefined label: 'products' ./RefMan-gal.v.tex:247: Warning: Undefined label: 'applications' ./RefMan-gal.v.tex:249: Warning: Undefined label: 'Implicits-explicitation' ./RefMan-gal.v.tex:250: Warning: Undefined label: 'scopechange' ./RefMan-gal.v.tex:254: Warning: Undefined label: 'caseanalysis' ./RefMan-gal.v.tex:255: Warning: Undefined label: 'qualid' ./RefMan-gal.v.tex:256: Warning: Undefined label: 'Gallina-sorts' ./RefMan-gal.v.tex:257: Warning: Undefined label: 'numerals' ./RefMan-gal.v.tex:258: Warning: Undefined label: 'hole' ./RefMan-gal.v.tex:262: Warning: Undefined label: 'Implicits-explicitation' ./RefMan-gal.v.tex:268: Warning: Undefined label: 'Binders' ./RefMan-gal.v.tex:362: Warning: Undefined label: 'Addoc-syntax' ./RefMan-gal.v.tex:364: Warning: Undefined label: 'libnats' ./RefMan-gal.v.tex:392: Warning: Undefined label: 'Sorts' ./RefMan-gal.v.tex:443: Warning: Undefined label: 'Binders' ./RefMan-gal.v.tex:450: Warning: Undefined label: 'let-in' ./RefMan-gal.v.tex:490: Warning: Undefined label: 'Implicits-explicitation' ./RefMan-gal.v.tex:532: Warning: Undefined label: 'Mult-match' ./RefMan-gal.v.tex:532: Warning: Undefined label: 'Mult-match-full' ./RefMan-gal.v.tex:604: Warning: Undefined label: 'Equality' ./RefMan-gal.v.tex:607: Warning: Undefined label: 'listn' ./RefMan-gal.v.tex:650: Warning: Undefined label: 'if-then-else' ./RefMan-gal.v.tex:650: Warning: Undefined label: 'Letin' ./RefMan-gal.v.tex:663: Warning: Undefined label: 'Fixpoint' ./RefMan-gal.v.tex:671: Warning: Undefined label: 'CoFixpoint' ./RefMan-gal.v.tex:740: Warning: Undefined label: 'sentences-syntax' ./RefMan-gal.v.tex:805: Warning: Undefined label: 'Section' ./RefMan-gal.v.tex:853: Warning: Undefined label: 'delta' ./RefMan-gal.v.tex:861: Warning: Undefined label: 'Typed-terms' ./RefMan-gal.v.tex:898: Warning: Undefined label: 'Opaque' ./RefMan-gal.v.tex:898: Warning: Undefined label: 'Transparent' ./RefMan-gal.v.tex:898: Warning: Undefined label: 'unfold' ./RefMan-gal.v.tex:918: Warning: Undefined label: 'Section' ./RefMan-gal.v.tex:918: Warning: Undefined label: 'Opaque' ./RefMan-gal.v.tex:919: Warning: Undefined label: 'Transparent' ./RefMan-gal.v.tex:919: Warning: Undefined label: 'unfold' ./RefMan-gal.v.tex:957: Warning: Undefined label: 'Positivity' ./RefMan-gal.v.tex:1186: Warning: Undefined label: 'Cic-inductive-definitions' ./RefMan-gal.v.tex:1186: Warning: Undefined label: 'Tac-induction' ./RefMan-gal.v.tex:1313: Warning: Undefined label: 'Section' ./RefMan-gal.v.tex:1339: Warning: Undefined label: 'gal_Inductive_Definitions' ./RefMan-gal.v.tex:1373: Warning: Undefined label: 'CoFixpoint' ./RefMan-gal.v.tex:1383: Warning: Undefined label: 'Function' ./RefMan-gal.v.tex:1436: Warning: Undefined label: 'Caseexpr' ./RefMan-gal.v.tex:1543: Warning: Undefined label: 'Scheme' ./RefMan-gal.v.tex:1555: Warning: Undefined label: 'CoInductiveTypes' ./RefMan-gal.v.tex:1623: Warning: Undefined label: 'Fixpoint' ./RefMan-gal.v.tex:1636: Warning: Undefined label: 'Proof-handling' ./RefMan-gal.v.tex:1636: Warning: Undefined label: 'Tactics' ./RefMan-gal.v.tex:1675: Warning: Undefined label: 'CoFixpoint' ./RefMan-gal.v.tex:1688: Warning: Undefined label: 'Guarded' ./RefMan-gal.v.tex:1697: Warning: Undefined label: 'Defined' ./RefMan-gal.v.tex:1703: Warning: Undefined label: 'Opaque' ./RefMan-gal.v.tex:1703: Warning: Undefined label: 'Transparent' ./RefMan-gal.v.tex:1704: Warning: Undefined label: 'unfold' ./RefMan-gal.v.tex:1736: Warning: Undefined label: 'Tactics' ./RefMan-gal.v.tex:1737: Warning: Undefined label: 'Proof-handling' ./RefMan-gal.v.tex:1757: Warning: Undefined label: 'Conversion-tactics' ./RefMan-gal.v.tex:1769: Warning: Undefined label: 'Conversion-tactics' ./RefMan-gal.v.tex:1769: Warning: Undefined label: 'Opaque' ./RefMan-gal.v.tex:1769: Warning: Undefined label: 'Transparent' ./RefMan-ext.v.tex:12: Warning: Undefined label: 'record-syntax' ./RefMan-ext.v.tex:166: Warning: Undefined label: 'Axiom' ./RefMan-ext.v.tex:168: Warning: Undefined label: 'Fixpoint' ./RefMan-ext.v.tex:168: Warning: Undefined label: 'Caseexpr' ./RefMan-ext.v.tex:182: Warning: Undefined label: 'gal_Inductive_Definitions' ./RefMan-ext.v.tex:186: Warning: Undefined label: 'Coercions-and-records' ./RefMan-ext.v.tex:212: Warning: Undefined label: 'Program' ./RefMan-ext.v.tex:257: Warning: Undefined label: 'fig:projsyntax' ./RefMan-ext.v.tex:287: Warning: Undefined label: 'SetPrintingMatching' ./RefMan-ext.v.tex:289: Warning: Undefined label: 'Mult-match-full' ./RefMan-ext.v.tex:348: Warning: Undefined label: 'printing-options' ./RefMan-ext.v.tex:389: Warning: Undefined label: 'printing-options' ./RefMan-ext.v.tex:433: Warning: Undefined label: 'printing-options' ./RefMan-ext.v.tex:687: Warning: Undefined label: 'FunInduction' ./RefMan-ext.v.tex:702: Warning: Undefined label: 'FunInduction' ./RefMan-ext.v.tex:703: Warning: Undefined label: 'FunScheme' ./RefMan-ext.v.tex:703: Warning: Undefined label: 'FunScheme-examples' ./RefMan-ext.v.tex:771: Warning: Undefined label: 'FunScheme' ./RefMan-ext.v.tex:771: Warning: Undefined label: 'FunScheme-examples' ./RefMan-ext.v.tex:771: Warning: Undefined label: 'FunInduction' ./RefMan-ext.v.tex:787: Warning: Undefined label: 'Inductive' ./RefMan-ext.v.tex:878: Warning: Undefined label: 'Basic-definitions' ./RefMan-mod.v.tex:33: Warning: Undefined label: 'Inline' ./RefMan-mod.v.tex:459: Warning: Undefined label: 'Notation' ./RefMan-ext.v.tex:974: Warning: Undefined label: 'qualid' ./RefMan-ext.v.tex:981: Warning: Undefined label: 'coqoptions' ./RefMan-ext.v.tex:983: Warning: Undefined label: 'coqoptions' ./RefMan-ext.v.tex:991: Warning: Undefined label: 'AddLoadPath' ./RefMan-ext.v.tex:991: Warning: Undefined label: 'AddRecLoadPath' ./RefMan-ext.v.tex:1029: Warning: Undefined label: 'Require' ./RefMan-ext.v.tex:1030: Warning: Undefined label: 'Import' ./RefMan-ext.v.tex:1073: Warning: Undefined label: 'Locate' ./RefMan-ext.v.tex:1074: Warning: Undefined label: 'Locate Library' ./RefMan-ext.v.tex:1172: Warning: Undefined label: 'SetReversiblePatternImplicit' ./RefMan-ext.v.tex:1192: Warning: Undefined label: 'ImplicitArguments' ./RefMan-ext.v.tex:1194: Warning: Undefined label: 'SetMaximalImplicitInsertion' ./RefMan-ext.v.tex:1195: Warning: Undefined label: 'PrintImplicit' ./RefMan-ext.v.tex:1372: Warning: Undefined label: 'PrintImplicit' ./RefMan-ext.v.tex:1388: Warning: Undefined label: 'SetStrictImplicit' ./RefMan-ext.v.tex:1388: Warning: Undefined label: 'SetContextualImplicit' ./RefMan-ext.v.tex:1388: Warning: Undefined label: 'SetReversiblePatternImplicit' ./RefMan-ext.v.tex:1389: Warning: Undefined label: 'SetMaximalImplicitInsertion' ./RefMan-ext.v.tex:1575: Warning: Undefined label: 'fig:explicitations' ./RefMan-ext.v.tex:1640: Warning: Undefined label: 'SetPrintingAll' ./RefMan-ext.v.tex:1913: Warning: Undefined label: 'Coercions-full' ./RefMan-ext.v.tex:1920: Warning: Undefined label: 'Addoc-syntax' ./RefMan-ext.v.tex:1947: Warning: Undefined label: 'Sorts' ./RefMan-ext.v.tex:1949: Warning: Undefined label: 'SetPrintingAll' ./RefMan-ext.v.tex:1960: Warning: Undefined label: 'Sorts' ./RefMan-lib.v.tex:15: Warning: Undefined label: 'Require' ./RefMan-lib.v.tex:21: Warning: Undefined label: 'Contributions' ./RefMan-lib.v.tex:48: Warning: Undefined label: 'init-notations' ./RefMan-lib.v.tex:119: Warning: Undefined label: 'formulas-syntax' ./RefMan-lib.v.tex:349: Warning: Undefined label: 'specif-syntax' ./RefMan-lib.v.tex:435: Warning: Undefined label: 'specif-syntax' ./RefMan-lib.v.tex:611: Warning: Undefined label: 'refine-example' ./RefMan-lib.v.tex:915: Warning: Undefined label: 'Other-commands' ./RefMan-lib.v.tex:924: Warning: Undefined label: 'zarith-syntax' ./RefMan-lib.v.tex:966: Warning: Undefined label: 'zarith-syntax' ./RefMan-lib.v.tex:998: Warning: Undefined label: 'nat-syntax' ./RefMan-lib.v.tex:1079: Warning: Undefined label: 'Tactics' ./RefMan-lib.v.tex:1162: Warning: Undefined label: 'TacticLanguage' ./RefMan-cic.v.tex:19: Warning: Undefined label: 'impredicativity' ./RefMan-cic.v.tex:31: Warning: Undefined label: 'Terms' ./RefMan-cic.v.tex:36: Warning: Undefined label: 'convertibility' ./RefMan-cic.v.tex:42: Warning: Undefined citation: 'GimCas05' ./RefMan-cic.v.tex:45: Warning: Undefined citation: 'CoqArt' ./RefMan-cic.v.tex:47: Warning: Undefined citation: 'Bar99' ./RefMan-cic.v.tex:47: Warning: Undefined citation: 'Wer94' ./RefMan-cic.v.tex:48: Warning: Undefined citation: 'Moh97' ./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu85a' ./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu85b' ./RefMan-cic.v.tex:49: Warning: Undefined citation: 'CoHu86' ./RefMan-cic.v.tex:50: Warning: Undefined citation: 'CoPa89' ./RefMan-cic.v.tex:53: Warning: Undefined citation: 'Bar91' ./RefMan-cic.v.tex:135: Warning: Undefined label: 'PrintingUniverses' ./RefMan-cic.v.tex:190: Warning: Undefined citation: 'Bar81' ./RefMan-cic.v.tex:269: Warning: Undefined label: 'Cic-inductive-definitions' ./RefMan-cic.v.tex:279: Warning: Undefined label: 'Cic-inductive-definitions' ./RefMan-cic.v.tex:349: Warning: Undefined label: 'conv-rules' ./RefMan-cic.v.tex:371: Warning: Undefined citation: 'Coq85' ./RefMan-cic.v.tex:375: Warning: Undefined label: 'iotared' ./RefMan-cic.v.tex:379: Warning: Undefined citation: 'Moh93' ./RefMan-cic.v.tex:379: Warning: Undefined citation: 'Wer94' ./RefMan-cic.v.tex:459: Warning: Undefined label: 'Tactics' ./RefMan-cic.v.tex:983: Warning: Undefined label: 'elimdep' ./RefMan-cic.v.tex:1025: Warning: Undefined label: 'singleton' ./RefMan-cic.v.tex:1027: Warning: Undefined label: 'impredicativity' ./RefMan-cic.v.tex:1034: Warning: Undefined label: 'elimdep' ./RefMan-cic.v.tex:1052: Warning: Undefined label: 'singleton' ./RefMan-cic.v.tex:1166: Warning: Undefined citation: 'Coq92' ./RefMan-cic.v.tex:1549: Warning: Undefined citation: 'Gim94' ./RefMan-cic.v.tex:1603: Warning: Undefined label: 'Fixpoint' ./RefMan-cic.v.tex:1774: Warning: Undefined label: 'Scheme' ./RefMan-cic.v.tex:1780: Warning: Undefined citation: 'Gimenez95b' ./RefMan-cic.v.tex:1780: Warning: Undefined citation: 'Gim98' ./RefMan-cic.v.tex:1780: Warning: Undefined citation: 'GimCas05' ./RefMan-modr.tex:47: Warning: Undefined label: 'Terms' ./RefMan-modr.tex:489: Warning: Undefined label: 'delta' ./RefMan-oth.v.tex:118: Warning: Undefined label: 'Conversion-tactics' ./RefMan-oth.v.tex:126: Warning: Undefined label: 'Conversion-tactics' ./RefMan-oth.v.tex:133: Warning: Undefined label: 'Sorts' ./RefMan-oth.v.tex:143: Warning: Undefined label: 'Extraction' ./RefMan-oth.v.tex:192: Warning: Undefined label: 'Require' ./RefMan-oth.v.tex:219: Warning: Undefined label: 'Notation' ./RefMan-oth.v.tex:226: Warning: Undefined label: 'scopechange' ./RefMan-oth.v.tex:458: Warning: Undefined label: 'LocateSymbol' ./RefMan-oth.v.tex:557: Warning: Undefined label: 'loadpath' ./RefMan-oth.v.tex:571: Warning: Undefined label: 'Begin-Silent' ./RefMan-oth.v.tex:581: Warning: Undefined label: 'Addoc-coqc' ./RefMan-oth.v.tex:605: Warning: Undefined label: 'loadpath' ./RefMan-oth.v.tex:614: Warning: Undefined label: 'Import' ./RefMan-oth.v.tex:655: Warning: Undefined label: 'loadpath' ./RefMan-oth.v.tex:682: Warning: Undefined label: 'Addoc-coqc' ./RefMan-oth.v.tex:697: Warning: Undefined label: 'loadpath' ./RefMan-oth.v.tex:700: Warning: Undefined label: 'Addoc-coqc' ./RefMan-oth.v.tex:711: Warning: Undefined label: 'Locate File' ./RefMan-oth.v.tex:718: Warning: Undefined label: 'LongNames' ./RefMan-oth.v.tex:792: Warning: Undefined label: 'compiled' ./RefMan-oth.v.tex:799: Warning: Undefined label: 'compiled' ./RefMan-oth.v.tex:808: Warning: Undefined label: 'compiled' ./RefMan-oth.v.tex:857: Warning: Undefined label: 'Proof-handling' ./RefMan-oth.v.tex:862: Warning: Undefined label: 'Proof-handling' ./RefMan-oth.v.tex:865: Warning: Undefined label: 'Proof-handling' ./RefMan-oth.v.tex:888: Warning: Undefined label: 'Proof-handling' ./RefMan-oth.v.tex:944: Warning: Undefined label: 'Pwd' ./RefMan-oth.v.tex:981: Warning: Undefined label: 'binary-images' ./RefMan-oth.v.tex:983: Warning: Undefined label: 'EnvVariables' ./RefMan-oth.v.tex:1068: Warning: Undefined citation: 'Leroy90' ./RefMan-oth.v.tex:1085: Warning: Undefined label: 'conv-rules' ./RefMan-oth.v.tex:1092: Warning: Undefined label: 'Conversion-tactics' ./RefMan-oth.v.tex:1092: Warning: Undefined label: 'Automatizing' ./RefMan-oth.v.tex:1093: Warning: Undefined label: 'Theorem' ./RefMan-oth.v.tex:1128: Warning: Undefined label: 'Conversion-tactics' ./RefMan-oth.v.tex:1128: Warning: Undefined label: 'Automatizing' ./RefMan-oth.v.tex:1129: Warning: Undefined label: 'Theorem' ./RefMan-oth.v.tex:1174: Warning: Undefined label: 'Conversion-tactics' ./RefMan-oth.v.tex:1194: Warning: Undefined label: 'vmcompute' ./RefMan-oth.v.tex:1194: Warning: Undefined label: 'vmoption' ./RefMan-oth.v.tex:1213: Warning: Undefined label: 'Coercions' ./RefMan-oth.v.tex:1214: Warning: Undefined label: 'Strategy' ./RefMan-oth.v.tex:1228: Warning: Undefined label: 'Implicit Arguments' ./RefMan-oth.v.tex:1229: Warning: Undefined label: 'TacticLanguage' ./RefMan-oth.v.tex:1230: Warning: Undefined label: 'Notation' ./RefMan-oth.v.tex:1243: Warning: Undefined label: 'Controlling reduction strategy' ./RefMan-pro.tex:5: Warning: Undefined label: 'Vernacular-commands' ./RefMan-pro.tex:10: Warning: Undefined label: 'Tactics' ./RefMan-pro.tex:24: Warning: Undefined label: 'Variable' ./RefMan-pro.tex:27: Warning: Undefined label: 'intro' ./RefMan-pro.tex:33: Warning: Undefined citation: 'How80' ./RefMan-pro.tex:33: Warning: Undefined citation: 'Bar91' ./RefMan-pro.tex:33: Warning: Undefined citation: 'Gir89' ./RefMan-pro.tex:33: Warning: Undefined citation: 'Hue89' ./RefMan-pro.tex:38: Warning: Undefined label: 'Resume' ./RefMan-pro.tex:55: Warning: Undefined label: 'Assertions' ./RefMan-pro.tex:125: Warning: Undefined label: 'exact' ./RefMan-pro.tex:134: Warning: Undefined label: 'ProofWith' ./RefMan-pro.tex:193: Warning: Undefined label: 'Show' ./RefMan-pro.tex:200: Warning: Undefined label: 'instantiate' ./RefMan-pro.tex:342: Warning: Undefined label: 'refine' ./RefMan-pro.tex:379: Warning: Undefined label: 'intro' ./RefMan-tac.v.tex:28: Warning: Undefined label: 'Show' ./RefMan-tac.v.tex:38: Warning: Undefined label: 'TacticLanguage' ./RefMan-tac.v.tex:68: Warning: Undefined label: 'conv-rules' ./RefMan-tac.v.tex:103: Warning: Undefined label: 'refine-example' ./RefMan-tac.v.tex:109: Warning: Undefined label: 'Cic' ./RefMan-tac.v.tex:116: Warning: Undefined label: 'Typed-terms' ./RefMan-tac.v.tex:255: Warning: Undefined label: 'Typed-terms' ./RefMan-tac.v.tex:303: Warning: Undefined label: 'LongNames' ./RefMan-tac.v.tex:313: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:366: Warning: Undefined label: 'move' ./RefMan-tac.v.tex:397: Warning: Undefined label: 'pattern' ./RefMan-tac.v.tex:407: Warning: Undefined label: 'pattern' ./RefMan-tac.v.tex:407: Warning: Undefined label: 'change' ./RefMan-tac.v.tex:437: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:458: Warning: Undefined label: 'eapply-example' ./RefMan-tac.v.tex:518: Warning: Undefined label: 'Occurrences clauses' ./RefMan-tac.v.tex:598: Warning: Undefined label: 'Typed-terms' ./RefMan-tac.v.tex:611: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:642: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:706: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:840: Warning: Undefined label: 'Conv' ./RefMan-tac.v.tex:876: Warning: Undefined label: 'Conversion-tactics' ./RefMan-tac.v.tex:884: Warning: Undefined label: 'Tac-induction' ./RefMan-tac.v.tex:899: Warning: Undefined label: 'Guarded' ./RefMan-tac.v.tex:931: Warning: Undefined label: 'Guarded' ./RefMan-tac.v.tex:996: Warning: Undefined label: 'PrintAssumptions' ./RefMan-tac.v.tex:1015: Warning: Undefined label: 'apply' ./RefMan-tac.v.tex:1065: Warning: Undefined label: 'elim' ./RefMan-tac.v.tex:1104: Warning: Undefined label: 'SetPrintingAll' ./RefMan-tac.v.tex:1106: Warning: Undefined label: 'Implicit Arguments' ./RefMan-tac.v.tex:1107: Warning: Undefined label: 'Coercions' ./RefMan-tac.v.tex:1133: Warning: Undefined label: 'tactic:set' ./RefMan-tac.v.tex:1133: Warning: Undefined label: 'Tac-induction' ./RefMan-tac.v.tex:1133: Warning: Undefined label: 'SetPrintingAll' ./RefMan-tac.v.tex:1212: Warning: Undefined label: 'tactic:set' ./RefMan-tac.v.tex:1212: Warning: Undefined label: 'rewrite' ./RefMan-tac.v.tex:1213: Warning: Undefined label: 'tactic:replace' ./RefMan-tac.v.tex:1214: Warning: Undefined label: 'tactic:autorewrite' ./RefMan-tac.v.tex:1250: Warning: Undefined label: 'Transparent' ./RefMan-tac.v.tex:1262: Warning: Undefined label: 'Opaque' ./RefMan-tac.v.tex:1355: Warning: Undefined label: 'Opaque' ./RefMan-tac.v.tex:1403: Warning: Undefined label: 'Basic-definitions' ./RefMan-tac.v.tex:1403: Warning: Undefined label: 'Transparent' ./RefMan-tac.v.tex:1445: Warning: Undefined label: 'scopechange' ./RefMan-tac.v.tex:1623: Warning: Undefined label: 'eapply-example' ./RefMan-tac.v.tex:1632: Warning: Undefined label: 'Cic-inductive-definitions' ./RefMan-tac.v.tex:1719: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:1730: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:1740: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:1748: Warning: Undefined label: 'eapply-example' ./RefMan-tac.v.tex:1772: Warning: Undefined label: 'Occurrences clauses' ./RefMan-tac.v.tex:1810: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:1905: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:1923: Warning: Undefined label: 'intros-pattern' ./RefMan-tac.v.tex:1930: Warning: Undefined label: 'Binding-list' ./RefMan-tac.v.tex:1938: Warning: Undefined label: 'eapply-example' ./RefMan-tac.v.tex:1951: Warning: Undefined label: 'Occurrences clauses' ./RefMan-tac.v.tex:2048: Warning: Undefined label: 'intro' ./RefMan-tac.v.tex:2055: Warning: Undefined label: 'destruct' ./RefMan-tac.v.tex:2082: Warning: Undefined label: 'clear' ./RefMan-tac.v.tex:2247: Warning: Undefined citation: 'DBLP:conf/types/McBride00' ./RefMan-tac.v.tex:2248: Warning: Undefined citation: 'DBLP:conf/types/CornesT95' ./RefMan-tac.v.tex:2351: Warning: Undefined label: 'dependent-induction-example' ./RefMan-tac.v.tex:2385: Warning: Undefined label: 'Record' ./RefMan-tac.v.tex:2396: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2397: Warning: Undefined label: 'FunScheme' ./RefMan-tac.v.tex:2437: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2438: Warning: Undefined label: 'FunScheme' ./RefMan-tac.v.tex:2441: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2445: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2447: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2450: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:2450: Warning: Undefined label: 'FunScheme' ./RefMan-tac.v.tex:2450: Warning: Undefined label: 'FunScheme-examples' ./RefMan-tac.v.tex:2451: Warning: Undefined label: 'sec:functional-inversion' ./RefMan-tac.v.tex:2466: Warning: Undefined label: 'Tac-induction' ./RefMan-tac.v.tex:2476: Warning: Undefined label: 'Tac-induction' ./RefMan-tac.v.tex:2480: Warning: Undefined label: 'Tac-induction' ./RefMan-tac.v.tex:2489: Warning: Undefined label: 'Equality' ./RefMan-tac.v.tex:2535: Warning: Undefined label: 'Conversion-tactics' ./RefMan-tac.v.tex:2558: Warning: Undefined label: 'pattern' ./RefMan-tac.v.tex:2640: Warning: Undefined label: 'Conversion-tactics' ./RefMan-tac.v.tex:2713: Warning: Undefined label: 'setoid_replace' ./RefMan-tac.v.tex:2915: Warning: Undefined label: 'Scheme' ./RefMan-tac.v.tex:3236: Warning: Undefined label: 'inversion-examples' ./RefMan-tac.v.tex:3272: Warning: Undefined label: 'inversion-examples' ./RefMan-tac.v.tex:3282: Warning: Undefined label: 'Function' ./RefMan-tac.v.tex:3318: Warning: Undefined label: 'quote-examples' ./RefMan-tac.v.tex:3373: Warning: Undefined label: 'Hints-databases' ./RefMan-tac.v.tex:3380: Warning: Undefined label: 'Hints-databases' ./RefMan-tac.v.tex:3408: Warning: Undefined label: 'Hints-databases' ./RefMan-tac.v.tex:3440: Warning: Undefined label: 'Hints-databases' ./RefMan-tac.v.tex:3485: Warning: Undefined citation: 'Dyc92' ./RefMan-tac.v.tex:3556: Warning: Undefined citation: 'Mun94' ./RefMan-tac.v.tex:3572: Warning: Undefined label: 'TacticLanguage' ./RefMan-tac.v.tex:3751: Warning: Undefined label: 'injection' ./RefMan-tac.v.tex:3751: Warning: Undefined label: 'discriminate' ./RefMan-tac.v.tex:3846: Warning: Undefined label: 'OmegaChapter' ./RefMan-tac.v.tex:3865: Warning: Undefined label: 'ring' ./RefMan-tac.v.tex:3891: Warning: Undefined label: 'ring' ./RefMan-tac.v.tex:3928: Warning: Undefined citation: 'Fourier' ./RefMan-tac.v.tex:3992: Warning: Undefined label: 'HintRewrite' ./RefMan-tac.v.tex:3994: Warning: Undefined label: 'autorewrite-example' ./RefMan-tac.v.tex:4010: Warning: Undefined label: 'PrintHint' ./RefMan-tac.v.tex:4030: Warning: Undefined label: 'HintTransparency' ./RefMan-tac.v.tex:4078: Warning: Undefined label: 'eauto' ./RefMan-tac.v.tex:4379: Warning: Undefined label: 'Section' ./RefMan-tac.v.tex:4430: Warning: Undefined label: 'BeginProof' ./RefMan-tac.v.tex:4527: Warning: Undefined label: 'Scheme-examples' ./RefMan-tac.v.tex:4558: Warning: Undefined label: 'CombinedScheme-examples' ./RefMan-tac.v.tex:4589: Warning: Undefined label: 'FunScheme-examples' ./RefMan-tac.v.tex:4612: Warning: Undefined label: 'Section' ./RefMan-tac.v.tex:4617: Warning: Undefined label: 'TacticLanguage' ./RefMan-ltac.v.tex:9: Warning: Undefined citation: 'Del00' ./RefMan-ltac.v.tex:9: Warning: Undefined label: 'Tactics-examples' ./RefMan-ltac.v.tex:29: Warning: Undefined label: 'ltac' ./RefMan-ltac.v.tex:30: Warning: Undefined label: 'ltac_aux' ./RefMan-ltac.v.tex:30: Warning: Undefined label: 'BNF-syntax' ./RefMan-ltac.v.tex:37: Warning: Undefined label: 'Tactics' ./RefMan-ltac.v.tex:56: Warning: Undefined label: 'ltactop' ./RefMan-ltac.v.tex:581: Warning: Undefined label: 'SetPrintingAll' ./RefMan-tacex.v.tex:476: Warning: Undefined label: 'FunInduction' ./RefMan-tacex.v.tex:515: Warning: Undefined label: 'Function' ./RefMan-tacex.v.tex:517: Warning: Undefined label: 'Function' ./RefMan-tacex.v.tex:1212: Warning: Undefined label: 'elim' ./RefMan-tacex.v.tex:1212: Warning: Undefined label: 'case' ./RefMan-tacex.v.tex:1212: Warning: Undefined label: 'inversion' ./RefMan-tacex.v.tex:1479: Warning: Undefined label: 'ring' ./RefMan-tacex.v.tex:1563: Warning: Undefined label: 'ring' ./RefMan-tacex.v.tex:1610: Warning: Undefined label: 'permutpred' ./RefMan-tacex.v.tex:1639: Warning: Undefined label: 'permutpred' ./RefMan-tacex.v.tex:1678: Warning: Undefined label: 'permutltac' ./RefMan-tacex.v.tex:1694: Warning: Undefined label: 'ltac' ./RefMan-tacex.v.tex:1811: Warning: Undefined citation: 'Dyc92' ./RefMan-tacex.v.tex:1812: Warning: Undefined label: 'tautoltaca' ./RefMan-tacex.v.tex:1813: Warning: Undefined label: 'tautoltacb' ./RefMan-tacex.v.tex:1848: Warning: Undefined citation: 'RC95' ./RefMan-tacex.v.tex:1849: Warning: Undefined label: 'isosax' ./RefMan-tacex.v.tex:1894: Warning: Undefined citation: 'RC95' ./RefMan-tacex.v.tex:1895: Warning: Undefined label: 'isosax' ./RefMan-tacex.v.tex:1985: Warning: Undefined label: 'isosltac1' ./RefMan-tacex.v.tex:1985: Warning: Undefined label: 'isosltac2' ./RefMan-decl.v.tex:125: Warning: Undefined label: 'lexical' ./RefMan-decl.v.tex:277: Warning: Undefined label: 'justifications' ./RefMan-decl.v.tex:1333: Warning: Undefined label: 'term-syntax-aux' ./RefMan-decl.v.tex:1488: Warning: Undefined citation: 'corbineau08types' ./RefMan-syn.v.tex:7: Warning: Undefined label: 'Notation' ./RefMan-syn.v.tex:10: Warning: Undefined label: 'scopes' ./RefMan-syn.v.tex:16: Warning: Undefined label: 'Abbreviations' ./RefMan-syn.v.tex:41: Warning: Undefined label: 'Abbreviations' ./RefMan-syn.v.tex:63: Warning: Undefined label: 'ReservedNotation' ./RefMan-syn.v.tex:128: Warning: Undefined label: 'init-notations' ./RefMan-syn.v.tex:223: Warning: Undefined label: 'Theories' ./RefMan-syn.v.tex:403: Warning: Undefined label: 'init-notations' ./RefMan-syn.v.tex:416: Warning: Undefined label: 'notation-syntax' ./RefMan-syn.v.tex:452: Warning: Undefined label: 'SetPrintingAll' ./RefMan-syn.v.tex:489: Warning: Undefined label: 'Locate' ./RefMan-syn.v.tex:641: Warning: Undefined label: 'scopes' ./RefMan-syn.v.tex:654: Warning: Undefined label: 'RecursiveNotations' ./RefMan-syn.v.tex:665: Warning: Undefined label: 'implicit-generalization' ./RefMan-syn.v.tex:696: Warning: Undefined label: 'notation-syntax' ./RefMan-syn.v.tex:697: Warning: Undefined label: 'scopes' ./RefMan-syn.v.tex:741: Warning: Undefined label: 'notation-syntax' ./RefMan-syn.v.tex:867: Warning: Undefined label: 'About' ./RefMan-syn.v.tex:883: Warning: Undefined label: 'Coercions-full' ./RefMan-syn.v.tex:923: Warning: Undefined label: 'About' ./RefMan-syn.v.tex:1019: Warning: Undefined label: 'strings' ./RefMan-com.tex:45: Warning: Undefined label: 'compiled' ./RefMan-com.tex:48: Warning: Undefined label: 'lexical' ./RefMan-com.tex:81: Warning: Undefined label: 'Makefile' ./RefMan-com.tex:107: Warning: Undefined label: 'LongNames' ./RefMan-com.tex:116: Warning: Undefined label: 'AddLoadPath' ./RefMan-com.tex:117: Warning: Undefined label: 'Libraries' ./RefMan-com.tex:126: Warning: Undefined label: 'AddRecLoadPath' ./RefMan-com.tex:127: Warning: Undefined label: 'Libraries' ./RefMan-com.tex:262: Warning: Undefined label: 'coqdoc' ./RefMan-com.tex:273: Warning: Undefined label: 'SetVirtualMachine' ./Helm.tex:24: Warning: Undefined label: 'Makefile' ./Helm.tex:73: Warning: Undefined label: 'coqdoc' ./Helm.tex:198: Warning: Undefined label: 'Section' ./RefMan-ide.tex:14: Warning: Undefined label: 'Addoc-coqc' ./RefMan-ide.tex:34: Warning: Undefined label: 'fig:coqide' ./RefMan-ide.tex:68: Warning: Undefined label: 'fig:coqide' ./RefMan-ide.tex:162: Warning: Undefined label: 'fig:querywindow' ./RefMan-ide.tex:193: Warning: Undefined label: 'sec:coqidecharencoding' ./RefMan-ide.tex:206: Warning: Undefined label: 'sec:trytactics' ./RefMan-ide.tex:236: Warning: Undefined label: 'Addoc-syntax' ./RefMan-ide.tex:310: Warning: Undefined label: 'Coqmktop' ./Cases.v.tex:14: Warning: Undefined label: 'term-syntax' ./Cases.v.tex:15: Warning: Undefined label: 'term-syntax-aux' ./Cases.v.tex:569: Warning: Undefined label: 'refine-example' ./Cases.v.tex:631: Warning: Undefined label: 'refine' ./Coercion.v.tex:41: Warning: Undefined label: 'fig:classes' ./Coercion.v.tex:206: Warning: Undefined label: 'sentences-syntax' ./Coercion.v.tex:227: Warning: Undefined label: 'sentences-syntax' ./Coercion.v.tex:330: Warning: Undefined label: 'Record' ./Classes.v.tex:18: Warning: Undefined citation: 'sozeau08' ./Classes.v.tex:49: Warning: \overrightarrow outside display mode ./Classes.v.tex:50: Warning: \overrightarrow outside display mode ./Classes.v.tex:169: Warning: Undefined label: 'classes:superclasses' ./Classes.v.tex:228: Warning: Undefined label: 'Variable' ./Classes.v.tex:336: Warning: Undefined label: 'SingletonClass' ./Classes.v.tex:420: Warning: Undefined label: 'Program' ./Classes.v.tex:450: Warning: Undefined label: 'SectionContext' ./Classes.v.tex:463: Warning: Undefined label: 'HintTransparency' ./Micromega.v.tex:5: Warning: Undefined label: 'sec:psatz-hurry' ./Micromega.v.tex:7: Warning: Undefined label: 'sec:psatz-back' ./Micromega.v.tex:9: Warning: Undefined label: 'sec:lia' ./Micromega.v.tex:87: Warning: Undefined label: 'ring' ./Micromega.v.tex:99: Warning: Undefined label: 'thm:psatz' ./Micromega.v.tex:125: Warning: Undefined label: 'OmegaChapter' ./Micromega.v.tex:126: Warning: Undefined citation: 'TheOmegaPaper' ./Extraction.v.tex:197: Warning: Undefined label: 'extraction:axioms' ./Extraction.v.tex:444: Warning: Undefined citation: 'Let02' ./Extraction.v.tex:605: Warning: Undefined citation: 'Let02' ./Program.v.tex:12: Warning: Undefined citation: 'Sozeau06' ./Program.v.tex:13: Warning: Undefined label: 'Extraction' ./Program.v.tex:17: Warning: Undefined citation: 'Rushby98' ./Program.v.tex:21: Warning: Undefined citation: 'Parent95b' ./Program.v.tex:43: Warning: Undefined label: 'Caseexpr' ./Program.v.tex:109: Warning: Undefined label: 'Basic-definitions' ./Program.v.tex:109: Warning: Undefined label: 'Fixpoint' ./Program.v.tex:149: Warning: Undefined label: 'Opaque' ./Program.v.tex:149: Warning: Undefined label: 'Transparent' ./Program.v.tex:149: Warning: Undefined label: 'unfold' ./Program.v.tex:156: Warning: Undefined label: 'Fixpoint' ./Polynom.v.tex:204: Warning: Undefined label: 'setoidtactics' ./Polynom.v.tex:373: Warning: Undefined label: 'setoidtactics' ./Polynom.v.tex:614: Warning: Undefined label: 'setoidtactics' ./Polynom.v.tex:905: Warning: Undefined label: 'ring' ./Polynom.v.tex:910: Warning: Undefined label: 'ring' ./Polynom.v.tex:932: Warning: Undefined citation: 'DelMay01' ./Polynom.v.tex:967: Warning: Undefined citation: 'Bou97' ./Polynom.v.tex:973: Warning: Undefined label: 'DiscussReflection' ./Nsatz.v.tex:16: Warning: Undefined label: 'setoidtactics' ./Nsatz.v.tex:54: Warning: Undefined label: 'typeclasses' ./Nsatz.v.tex:74: Warning: Undefined citation: 'sugar' ./Setoid.v.tex:143: Warning: Undefined label: 'setoidtactics' ./Setoid.v.tex:333: Warning: Undefined label: 'setoid:first-class' ./Setoid.v.tex:474: Warning: Undefined label: 'typeclasses' ./Setoid.v.tex:725: Warning: Undefined label: 'TypeclassesTransparency' ./Reference-Manual.bbl:122: Warning: Undefined citation: 'DBLP:conf/types/2002' ./Reference-Manual.bbl:146: Warning: Undefined citation: 'CoC89' ./Reference-Manual.bbl:157: Warning: Undefined citation: 'Bastad92' ./Reference-Manual.bbl:162: Warning: Undefined citation: 'Nijmegen93' ./Reference-Manual.bbl:206: Warning: Undefined citation: 'DBLP:conf/types/1995' ./Reference-Manual.bbl:358: Warning: Undefined citation: 'Filliatre99' ./Reference-Manual.bbl:471: Warning: Undefined citation: 'Hue87tapsoft' ./Reference-Manual.bbl:484: Warning: Undefined citation: 'CoC89' ./Reference-Manual.bbl:552: Warning: Undefined citation: 'DBLP:conf/types/2002' ./Reference-Manual.bbl:585: Warning: Undefined citation: 'DBLP:conf/types/2000' ./Reference-Manual.bbl:610: Warning: Undefined citation: 'DBLP:conf/types/2002' ./Reference-Manual.bbl:660: Warning: Undefined citation: 'Nijmegen93' HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. Run, run, again... Exclude comment 'comment' ./Classes.v.tex:49: Warning: \overrightarrow outside display mode ./Classes.v.tex:50: Warning: \overrightarrow outside display mode Fixpoint reached in 2 step(s) install -m 644 doc/common/styles/html/simple/cover.html doc/refman rm -rf doc/refman/html install -d doc/refman/html install -m 644 doc/refman/coqide.png doc/refman/coqide-queries.png doc/refman/html (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) install -m 644 doc/refman/cover.html doc/refman/html/index.html install -m 644 doc/common/styles/html/simple/*.css doc/refman/html (cd `dirname doc/refman/Reference-Manual.dvi`; dvips -q -o `basename doc/refman/Reference-Manual.ps` `basename doc/refman/Reference-Manual.dvi`) (cd doc/refman;\ pdflatex -interaction=batchmode Reference-Manual.tex;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' ***************************************************** ***************************************************** ****************** Entering stage2 ****************** ***************************************************** ***************************************************** /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage2 "faq" make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' (cd `dirname doc/faq/FAQ.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/faq/FAQ.tex`) Your version of coqtop seems OK (cd doc/faq;\ latex -interaction=batchmode FAQ.v;\ BIBINPUTS=.: bibtex -min-crossrefs=10 -terse FAQ.v;\ latex -interaction=batchmode FAQ.v > /dev/null;\ latex -interaction=batchmode FAQ.v > /dev/null;\ ../tools/show_latex_messages FAQ.v.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode LaTeX Font Warning: Font shape `OT1/cmr/bx/sc' undefined LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined Overfull \hbox (15.0pt too wide) in paragraph at lines 517--520 (file FAQ.v.tex) LaTeX Font Warning: Font shape `OMS/cmtt/m/it' undefined Overfull \hbox (2.0598pt too wide) in paragraph at lines 3461--3465 (file FAQ.v.tex) LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined LaTeX Font Warning: Some font shapes were not available, defaults substituted. (cd doc/faq; (hevea -fix -exec xxdate.exe FAQ.v.tex 2>&1 | grep -v "^Warning: List with no item")) Exclude comment 'comment' ./FAQ.v.tex:143: Warning: Undefined label: 'lastquestion' ./FAQ.v.tex:157: Warning: File \jobname.htoc not found ./FAQ.v.tex:252: Warning: Undefined citation: 'ProofsTypes' ./FAQ.v.tex:253: Warning: Undefined citation: 'Types:Dowek' ./FAQ.v.tex:255: Warning: Undefined citation: 'Pau96b' ./FAQ.v.tex:257: Warning: Undefined citation: 'EGThese' ./FAQ.v.tex:367: Warning: Undefined citation: 'Coq:manual' ./FAQ.v.tex:368: Warning: Undefined citation: 'Coq:Tutorial' ./FAQ.v.tex:387: Warning: Undefined label: 'coqbug' ./FAQ.v.tex:412: Warning: Undefined citation: 'Coq:manual' ./FAQ.v.tex:413: Warning: Undefined citation: 'Coq:coqart' ./FAQ.v.tex:451: Warning: Undefined citation: 'CoHu86' ./FAQ.v.tex:452: Warning: Undefined citation: 'Luo90' ./FAQ.v.tex:453: Warning: Undefined citation: 'CoPa89' ./FAQ.v.tex:543: Warning: Undefined citation: 'HofStr98' ./FAQ.v.tex:558: Warning: Undefined label: 'proof-irrelevance' ./FAQ.v.tex:560: Warning: Undefined citation: 'HofStr98' ./FAQ.v.tex:568: Warning: Undefined citation: 'HofStr98' ./FAQ.v.tex:710: Warning: Undefined label: 'proof-irrelevance' ./FAQ.v.tex:716: Warning: Undefined label: 'le-uniqueness' ./FAQ.v.tex:728: Warning: Undefined citation: 'HofStr98' ./FAQ.v.tex:729: Warning: Undefined label: 'proof-irrelevance' ./FAQ.v.tex:794: Warning: Undefined citation: 'Gir70' ./FAQ.v.tex:794: Warning: Undefined citation: 'Coq85' ./FAQ.v.tex:2166: Warning: Undefined label: 'opaque' ./FAQ.v.tex:2459: Warning: Undefined label: 'implicit' ./FAQ.v.tex:2782: Warning: Undefined citation: 'coqart' ./FAQ.v.tex:2785: Warning: Undefined label: 'minmax' ./FAQ.v.tex:3180: Warning: Undefined label: 'forallcoqide' ./FAQ.v.tex:3399: Warning: Undefined label: 'K-nat' ./FAQ.v.tex:3698: Warning: Undefined label: 'inputmeth' ./FAQ.v.tex:3830: Warning: Undefined citation: 'howe' ./FAQ.v.tex:3830: Warning: Undefined citation: 'harrison' ./FAQ.v.tex:3830: Warning: Undefined citation: 'boutin' ./FAQ.v.tex:3840: Warning: Undefined label: 'proof-irrelevance' ./FAQ.v.tex:3978: Warning: Undefined citation: 'Coq:manual' ./FAQ.v.tex:3979: Warning: Undefined citation: 'Coq:coqart' ./FAQ.v.tex:3982: Warning: Undefined citation: 'Coq:Tutorial' ********************************************* ********* That makes 177 questions ********** ********************************************* HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. Run, run, again... Exclude comment 'comment' ./FAQ.v.htoc:20: Warning: List with no item ./FAQ.v.htoc:34: Warning: List with no item ./FAQ.v.htoc:42: Warning: List with no item ./FAQ.v.htoc:193: Warning: List with no item ./FAQ.v.htoc:207: Warning: List with no item ./FAQ.v.htoc:213: Warning: List with no item ./FAQ.v.htoc:226: Warning: List with no item ./FAQ.v.htoc:238: Warning: List with no item ./FAQ.v.htoc:252: Warning: List with no item ./FAQ.v.htoc:260: Warning: List with no item ./FAQ.v.htoc:275: Warning: List with no item ./FAQ.v.htoc:288: Warning: List with no item ./FAQ.v.htoc:294: Warning: List with no item ********************************************* ********* That makes 177 questions ********** ********************************************* Fixpoint reached in 2 step(s) rm -rf doc/faq/html install -d doc/faq/html install -m 644 doc/faq/interval_discr.v doc/faq/axioms.png doc/faq/html install -m 644 doc/faq/FAQ.v.html doc/faq/html/index.html (cd `dirname doc/faq/FAQ.v.dvi`; dvips -q -o `basename doc/faq/FAQ.v.ps` `basename doc/faq/FAQ.v.dvi`) (cd doc/faq;\ pdflatex -interaction=batchmode FAQ.v.tex;\ ../tools/show_latex_messages FAQ.v.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode LaTeX Font Warning: Font shape `OT1/cmr/bx/sc' undefined LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined Overfull \hbox (15.0pt too wide) in paragraph at lines 515--520 (file FAQ.v.tex) LaTeX Font Warning: Font shape `OMS/cmtt/m/it' undefined Overfull \hbox (2.0598pt too wide) in paragraph at lines 3461--3465 (file FAQ.v.tex) LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined LaTeX Font Warning: Some font shapes were not available, defaults substituted. make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' ***************************************************** ***************************************************** ****************** Entering stage2 ****************** ***************************************************** ***************************************************** /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage2 "tutorial" make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' (cd `dirname doc/tutorial/Tutorial.tex`; /build/buildd/coq-doc-8.3pl4/bin/coq-tex -n 72 -image "/build/buildd/coq-doc-8.3pl4/bin/coqtop -boot" -sl -small `basename doc/tutorial/Tutorial.tex`) Your version of coqtop seems OK (cd doc/tutorial; hevea -fix -exec xxdate.exe Tutorial.v) ../common/macros.tex:207: Warning: Defining '\proof' by \renewcommand ./Tutorial.v.tex:13: Warning: Command not found: \vfill ./Tutorial.v.tex:13: Warning: \hbox ./Tutorial.v.tex:13: Warning: Command not found: \vfill HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. Run, run, again... ../common/macros.tex:207: Warning: Defining '\proof' by \renewcommand ./Tutorial.v.tex:13: Warning: Command not found: \vfill ./Tutorial.v.tex:13: Warning: \hbox ./Tutorial.v.tex:13: Warning: Command not found: \vfill Fixpoint reached in 2 step(s) (cd doc/tutorial;\ latex -interaction=batchmode Tutorial.v;\ ../tools/show_latex_messages Tutorial.v.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode Overfull \hbox (7.19824pt too wide) in paragraph at lines 1158--1158 (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) (cd `dirname doc/tutorial/Tutorial.v.dvi`; dvips -q -o `basename doc/tutorial/Tutorial.v.ps` `basename doc/tutorial/Tutorial.v.dvi`) (cd doc/tutorial;\ pdflatex -interaction=batchmode Tutorial.v.tex;\ ../tools/show_latex_messages Tutorial.v.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode Overfull \hbox (7.19824pt too wide) in paragraph at lines 1158--1158 (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) Overfull \hbox (41.43161pt too wide) has occurred while \output is active (file Tutorial.v.tex) make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' ***************************************************** ***************************************************** ****************** Entering stage2 ****************** ***************************************************** ***************************************************** /usr/bin/make --warn-undefined-variable --no-builtin-rules -f Makefile.stage2 "rectutorial" make[3]: Entering directory `/build/buildd/coq-doc-8.3pl4' (cd doc/RecTutorial; hevea -fix -exec xxdate.exe RecTutorial) ./RecTutorial.tex:42: Warning: Defining '\familydefault' by \renewcommand ./RecTutorial.tex:43: Warning: Defining '\seriesdefault' by \renewcommand ./RecTutorial.tex:44: Warning: Defining '\shapedefault' by \renewcommand ./RecTutorial.tex:67: Warning: File \jobname.htoc not found ./RecTutorial.tex:81: Warning: Undefined citation: 'Coquand:metamathematical' ./RecTutorial.tex:82: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:84: Warning: Undefined citation: 'coqsite' ./RecTutorial.tex:85: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:86: Warning: Undefined citation: 'Booksite' ./RecTutorial.tex:90: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:110: Warning: Undefined label: 'CaseAnalysis' ./RecTutorial.tex:116: Warning: Undefined label: 'Introduction' ./RecTutorial.tex:116: Warning: Undefined label: 'CaseTechniques' ./RecTutorial.tex:118: Warning: Undefined label: 'StructuralInduction' ./RecTutorial.tex:120: Warning: Undefined label: 'CaseStudy' ./RecTutorial.tex:122: Warning: Undefined label: 'CoInduction' ./RecTutorial.tex:212: Warning: Undefined label: 'StructuralInduction' ./RecTutorial.tex:230: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:398: Warning: Undefined label: 'vectors' ./RecTutorial.tex:528: Warning: Undefined label: 'WellFoundedRecursion' ./RecTutorial.tex:574: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:574: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:707: Warning: Undefined label: 'WellFoundedRecursion' ./RecTutorial.tex:880: Warning: Command not found: \boldsymbol ./RecTutorial.tex:880: Warning: Command not found: \boldsymbol ./RecTutorial.tex:900: Warning: Undefined label: 'inversion' ./RecTutorial.tex:904: Warning: Undefined label: 'firstpred' ./RecTutorial.tex:1382: Warning: Undefined label: 'CaseScheme' ./RecTutorial.tex:1582: Warning: Undefined label: 'ex-def' ./RecTutorial.tex:1586: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:1641: Warning: Undefined label: 'MutuallyDependent' ./RecTutorial.tex:1686: Warning: Undefined citation: 'Bar98' ./RecTutorial.tex:1686: Warning: Undefined citation: 'Coq86' ./RecTutorial.tex:1770: Warning: Undefined citation: 'Coq86' ./RecTutorial.tex:1838: Warning: Undefined label: 'Discrimination' ./RecTutorial.tex:1894: Warning: Defining '\multirowsetup' by \renewcommand ./RecTutorial.tex:1899: Warning: Command not found: \multirow ./RecTutorial.tex:1903: Warning: \cline changed into \hline ./RecTutorial.tex:1905: Warning: \cline changed into \hline ./RecTutorial.tex:1907: Warning: \cline changed into \hline ./RecTutorial.tex:1925: Warning: Undefined label: 'Introduction' ./RecTutorial.tex:1939: Warning: Undefined label: 'Introduction' ./RecTutorial.tex:2086: Warning: Undefined label: 'DependentCase' ./RecTutorial.tex:2108: Warning: Undefined label: 'Introduction' ./RecTutorial.tex:2705: Warning: Undefined label: 'natdoublerect' ./RecTutorial.tex:2828: Warning: Undefined label: 'parameterstuff' ./RecTutorial.tex:2859: Warning: Undefined label: 'parameterstuff' ./RecTutorial.tex:3077: Warning: Undefined label: 'vectors' ./RecTutorial.tex:3123: Warning: Undefined citation: 'conor:motive' ./RecTutorial.tex:3156: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:3346: Warning: Undefined citation: 'EG96' ./RecTutorial.tex:3346: Warning: Undefined citation: 'EG95a' ./RecTutorial.tex:3367: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:3400: Warning: Undefined citation: 'EG94a' ./RecTutorial.tex:3451: Warning: Undefined citation: 'EG95a' ./RecTutorial.tex:3532: Warning: Undefined label: 'WellFoundedRecursion' ./RecTutorial.tex:3577: Warning: Undefined label: 'zeroton' ./RecTutorial.tex:3582: Warning: Undefined label: 'CaseTechniques' HeVeA Warning: Label(s) may have changed. Rerun me to get cross-references right. Run, run, again... ./RecTutorial.tex:42: Warning: Defining '\familydefault' by \renewcommand ./RecTutorial.tex:43: Warning: Defining '\seriesdefault' by \renewcommand ./RecTutorial.tex:44: Warning: Defining '\shapedefault' by \renewcommand ./RecTutorial.tex:81: Warning: Undefined citation: 'Coquand:metamathematical' ./RecTutorial.tex:82: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:84: Warning: Undefined citation: 'coqsite' ./RecTutorial.tex:85: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:86: Warning: Undefined citation: 'Booksite' ./RecTutorial.tex:90: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:230: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:574: Warning: Undefined citation: 'coqrefman' ./RecTutorial.tex:574: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:880: Warning: Command not found: \boldsymbol ./RecTutorial.tex:880: Warning: Command not found: \boldsymbol ./RecTutorial.tex:1586: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:1686: Warning: Undefined citation: 'Bar98' ./RecTutorial.tex:1686: Warning: Undefined citation: 'Coq86' ./RecTutorial.tex:1770: Warning: Undefined citation: 'Coq86' ./RecTutorial.tex:1894: Warning: Defining '\multirowsetup' by \renewcommand ./RecTutorial.tex:1899: Warning: Command not found: \multirow ./RecTutorial.tex:1903: Warning: \cline changed into \hline ./RecTutorial.tex:1905: Warning: \cline changed into \hline ./RecTutorial.tex:1907: Warning: \cline changed into \hline ./RecTutorial.tex:3123: Warning: Undefined citation: 'conor:motive' ./RecTutorial.tex:3156: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:3346: Warning: Undefined citation: 'EG96' ./RecTutorial.tex:3346: Warning: Undefined citation: 'EG95a' ./RecTutorial.tex:3367: Warning: Undefined citation: 'coqart' ./RecTutorial.tex:3400: Warning: Undefined citation: 'EG94a' ./RecTutorial.tex:3451: Warning: Undefined citation: 'EG95a' Fixpoint reached in 2 step(s) (cd doc/RecTutorial;\ latex -interaction=batchmode RecTutorial;\ BIBINPUTS=.: bibtex -min-crossrefs=10 -terse RecTutorial;\ latex -interaction=batchmode RecTutorial > /dev/null;\ latex -interaction=batchmode RecTutorial > /dev/null;\ ../tools/show_latex_messages RecTutorial.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode (cd `dirname doc/RecTutorial/RecTutorial.dvi`; dvips -q -o `basename doc/RecTutorial/RecTutorial.ps` `basename doc/RecTutorial/RecTutorial.dvi`) (cd doc/RecTutorial;\ pdflatex -interaction=batchmode RecTutorial.tex;\ ../tools/show_latex_messages RecTutorial.log) This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2012/dev/Debian) restricted \write18 enabled. entering extended mode make[3]: Leaving directory `/build/buildd/coq-doc-8.3pl4' make[2]: Leaving directory `/build/buildd/coq-doc-8.3pl4' make[1]: Leaving directory `/build/buildd/coq-doc-8.3pl4' dh_testroot dh_prep dh_installdirs dh_install dh_installdocs dh_installchangelogs dh_installexamples dh_installman dh_installcatalogs dh_installcron dh_installdebconf dh_installemacsen dh_installifupdown dh_installinfo dh_installinit dh_installmenu dh_installmime dh_installmodules dh_installlogcheck dh_installlogrotate dh_installpam dh_installppp dh_installudev dh_installwm dh_installxfonts dh_installgsettings dh_bugfiles dh_ucf dh_lintian dh_gconf dh_icons dh_perl dh_usrlocal dh_link dh_compress dh_fixperms dh_installdeb dh_gencontrol dh_md5sums dh_builddeb INFO: pkgstriptranslations version 116 pkgstriptranslations: processing coq-doc (in debian/coq-doc); do_strip: , oemstrip: pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/coq-doc/DEBIAN/control, package coq-doc, directory debian/coq-doc Searching for duplicated docs in dependency coq-doc-html... symlinking changelog.Debian.gz in coq-doc to file in coq-doc-html Searching for duplicated docs in dependency coq-doc-pdf... pkgstripfiles: Disabled PNG optimization for -doc package coq-doc (to save build time) dpkg-deb: warning: 'debian/coq-doc/DEBIAN/control' contains user-defined field 'Original-Maintainer' dpkg-deb: warning: ignoring 1 warning about the control file(s) dpkg-deb: building package `coq-doc' in `../coq-doc_8.3pl4-1_all.deb'. INFO: pkgstriptranslations version 116 pkgstriptranslations: processing coq-doc-html (in debian/coq-doc-html); do_strip: , oemstrip: pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/coq-doc-html/DEBIAN/control, package coq-doc-html, directory debian/coq-doc-html pkgstripfiles: Truncating usr/share/doc/coq-doc-html/changelog.Debian.gz to topmost ten records OptiPNG 0.6.4: Advanced PNG optimizer. Copyright (C) 2001-2010 Cosmin Truta. ** Processing: ./usr/share/doc/coq-doc-html/refman/coqide.png 854x535 pixels, 4x8 bits/pixel, RGB+alpha Reducing image to 3x8 bits/pixel, RGB Input IDAT size = 20856 bytes Input file size = 20953 bytes Trying: zc = 9 zm = 8 zs = 0 f = 0 IDAT size = 17222 zc = 9 zm = 8 zs = 1 f = 0 zc = 1 zm = 8 zs = 2 f = 0 zc = 9 zm = 8 zs = 3 f = 0 zc = 9 zm = 8 zs = 0 f = 1 zc = 9 zm = 8 zs = 1 f = 1 zc = 1 zm = 8 zs = 2 f = 1 zc = 9 zm = 8 zs = 3 f = 1 zc = 9 zm = 8 zs = 0 f = 2 zc = 9 zm = 8 zs = 1 f = 2 zc = 1 zm = 8 zs = 2 f = 2 zc = 9 zm = 8 zs = 3 f = 2 zc = 9 zm = 8 zs = 0 f = 3 zc = 9 zm = 8 zs = 1 f = 3 zc = 1 zm = 8 zs = 2 f = 3 zc = 9 zm = 8 zs = 3 f = 3 zc = 9 zm = 8 zs = 0 f = 4 zc = 9 zm = 8 zs = 1 f = 4 zc = 1 zm = 8 zs = 2 f = 4 zc = 9 zm = 8 zs = 3 f = 4 zc = 9 zm = 8 zs = 0 f = 5 zc = 9 zm = 8 zs = 1 f = 5 zc = 1 zm = 8 zs = 2 f = 5 zc = 9 zm = 8 zs = 3 f = 5 Selecting parameters: zc = 9 zm = 8 zs = 0 f = 0 IDAT size = 17222 Output IDAT size = 17222 bytes (3634 bytes decrease) Output file size = 17294 bytes (3659 bytes = 17.46% decrease) 17294 15594 90% ./usr/share/doc/coq-doc-html/refman/coqide.png 17294 15594 90% OptiPNG 0.6.4: Advanced PNG optimizer. Copyright (C) 2001-2010 Cosmin Truta. ** Processing: ./usr/share/doc/coq-doc-html/refman/coqide-queries.png 852x515 pixels, 4x8 bits/pixel, RGB+alpha Reducing image to 3x8 bits/pixel, RGB Input IDAT size = 27207 bytes Input file size = 27316 bytes Trying: zc = 9 zm = 8 zs = 0 f = 0 IDAT size = 22549 zc = 9 zm = 8 zs = 1 f = 0 zc = 1 zm = 8 zs = 2 f = 0 zc = 9 zm = 8 zs = 3 f = 0 zc = 9 zm = 8 zs = 0 f = 1 zc = 9 zm = 8 zs = 1 f = 1 zc = 1 zm = 8 zs = 2 f = 1 zc = 9 zm = 8 zs = 3 f = 1 zc = 9 zm = 8 zs = 0 f = 2 zc = 9 zm = 8 zs = 1 f = 2 zc = 1 zm = 8 zs = 2 f = 2 zc = 9 zm = 8 zs = 3 f = 2 zc = 9 zm = 8 zs = 0 f = 3 zc = 9 zm = 8 zs = 1 f = 3 zc = 1 zm = 8 zs = 2 f = 3 zc = 9 zm = 8 zs = 3 f = 3 zc = 9 zm = 8 zs = 0 f = 4 zc = 9 zm = 8 zs = 1 f = 4 zc = 1 zm = 8 zs = 2 f = 4 zc = 9 zm = 8 zs = 3 f = 4 zc = 9 zm = 8 zs = 0 f = 5 zc = 9 zm = 8 zs = 1 f = 5 zc = 1 zm = 8 zs = 2 f = 5 zc = 9 zm = 8 zs = 3 f = 5 Selecting parameters: zc = 9 zm = 8 zs = 0 f = 0 IDAT size = 22549 Output IDAT size = 22549 bytes (4658 bytes decrease) Output file size = 22621 bytes (4695 bytes = 17.19% decrease) 22621 20752 91% ./usr/share/doc/coq-doc-html/refman/coqide-queries.png 22621 20752 91% pkgstripfiles: PNG optimization for package coq-doc-html took 7 s dpkg-deb: warning: 'debian/coq-doc-html/DEBIAN/control' contains user-defined field 'Original-Maintainer' dpkg-deb: warning: ignoring 1 warning about the control file(s) dpkg-deb: building package `coq-doc-html' in `../coq-doc-html_8.3pl4-1_all.deb'. INFO: pkgstriptranslations version 116 pkgstriptranslations: processing coq-doc-pdf (in debian/coq-doc-pdf); do_strip: , oemstrip: pkgmaintainermangler: Maintainer field overridden to "Ubuntu Developers " pkgstripfiles: processing control file: debian/coq-doc-pdf/DEBIAN/control, package coq-doc-pdf, directory debian/coq-doc-pdf pkgstripfiles: Truncating usr/share/doc/coq-doc-pdf/changelog.Debian.gz to topmost ten records pkgstripfiles: PNG optimization for package coq-doc-pdf took 0 s dpkg-deb: warning: 'debian/coq-doc-pdf/DEBIAN/control' contains user-defined field 'Original-Maintainer' dpkg-deb: warning: ignoring 1 warning about the control file(s) dpkg-deb: building package `coq-doc-pdf' in `../coq-doc-pdf_8.3pl4-1_all.deb'. dpkg-genchanges -b -mUbuntu/amd64 Build Daemon >../coq-doc_8.3pl4-1_i386.changes dpkg-genchanges: binary-only upload - not including any source code dpkg-source --after-build coq-doc-8.3pl4 dpkg-buildpackage: binary only upload (no source included) ****************************************************************************** Build finished at 20120502-0749 chroot-autobuild/build/buildd/coq-doc_8.3pl4-1_all.deb: new debian package, version 2.0. size 4578 bytes: control archive= 619 bytes. 682 bytes, 17 lines control 66 bytes, 1 lines md5sums Package: coq-doc Version: 8.3pl4-1 Architecture: all Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 40 Depends: coq-doc-html (>= 8.3pl4-1), coq-doc-pdf (>= 8.3pl4-1) Section: non-free/doc Priority: optional Homepage: http://coq.inria.fr/ Description: documentation for Coq 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 Camlp5. . This is a dummy package which will install the documentation in html and pdf formats. chroot-autobuild/build/buildd/coq-doc-html_8.3pl4-1_all.deb: new debian package, version 2.0. size 505154 bytes: control archive= 1994 bytes. 674 bytes, 17 lines control 4445 bytes, 51 lines md5sums Package: coq-doc-html Source: coq-doc Version: 8.3pl4-1 Architecture: all Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 2423 Replaces: coq-doc (<= 8.0pl1.0-1) Section: non-free/doc Priority: optional Homepage: http://coq.inria.fr/ Description: documentation for Coq in html format 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 Camlp5. . This package contains its documentation and tutorials in html format. chroot-autobuild/build/buildd/coq-doc-pdf_8.3pl4-1_all.deb: new debian package, version 2.0. size 2374790 bytes: control archive= 912 bytes. 671 bytes, 17 lines control 740 bytes, 10 lines md5sums Package: coq-doc-pdf Source: coq-doc Version: 8.3pl4-1 Architecture: all Maintainer: Ubuntu Developers Original-Maintainer: Debian OCaml Maintainers Installed-Size: 2353 Replaces: coq-doc (<= 8.0pl1.0-1) Section: non-free/doc Priority: optional Homepage: http://coq.inria.fr/ Description: documentation for Coq in pdf format 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 Camlp5. . This package contains its documentation and tutorials in pdf format. chroot-autobuild/build/buildd/coq-doc_8.3pl4-1_all.deb: drwxr-xr-x root/root 0 2012-05-02 07:49 ./ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc/ -rw-r--r-- root/root 9966 2012-04-06 05:31 ./usr/share/doc/coq-doc/copyright drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/coq/ lrwxrwxrwx root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc/pdf -> ../coq-doc-pdf lrwxrwxrwx root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc/html -> ../coq-doc-html lrwxrwxrwx root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc/changelog.Debian.gz -> ../coq-doc-html/changelog.Debian.gz lrwxrwxrwx root/root 0 2012-05-02 07:49 ./usr/share/doc/coq/pdf -> ../coq-doc-pdf lrwxrwxrwx root/root 0 2012-05-02 07:49 ./usr/share/doc/coq/html -> ../coq-doc-html chroot-autobuild/build/buildd/coq-doc-html_8.3pl4-1_all.deb: drwxr-xr-x root/root 0 2012-05-02 07:49 ./ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/refman/ -rw-r--r-- root/root 129258 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual003.html -rw-r--r-- root/root 80454 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual009.html -rw-r--r-- root/root 1034 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual020.html -rw-r--r-- root/root 21206 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual010.html -rw-r--r-- root/root 90659 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual013.html -rw-r--r-- root/root 42901 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual002.html -rw-r--r-- root/root 197 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/style.css -rw-r--r-- root/root 67735 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual015.html -rw-r--r-- root/root 3344 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual021.html -rw-r--r-- root/root 283144 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual011.html -rw-r--r-- root/root 2162 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/index.html -rw-r--r-- root/root 39418 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/command-index.html -rw-r--r-- root/root 126067 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual004.html -rw-r--r-- root/root 21721 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual017.html -rw-r--r-- root/root 64588 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual005.html -rw-r--r-- root/root 726 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual008.html -rw-r--r-- root/root 8653 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual030.html -rw-r--r-- root/root 15594 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/refman/coqide.png -rw-r--r-- root/root 57548 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual029.html -rw-r--r-- root/root 56188 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual018.html -rw-r--r-- root/root 21001 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/error-index.html -rw-r--r-- root/root 1646 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual016.html -rw-r--r-- root/root 20708 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual028.html -rw-r--r-- root/root 42025 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual023.html -rw-r--r-- root/root 9382 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual001.html -rw-r--r-- root/root 20752 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/refman/coqide-queries.png -rw-r--r-- root/root 32840 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual027.html -rw-r--r-- root/root 132762 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual006.html -rw-r--r-- root/root 9816 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual025.html -rw-r--r-- root/root 60422 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual012.html -rw-r--r-- root/root 99882 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/general-index.html -rw-r--r-- root/root 34596 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual022.html -rw-r--r-- root/root 65593 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual014.html -rw-r--r-- root/root 47991 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual031.html -rw-r--r-- root/root 1830 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/hevea.css -rw-r--r-- root/root 40819 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/biblio.html -rw-r--r-- root/root 16572 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual026.html -rw-r--r-- root/root 51246 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual007.html -rw-r--r-- root/root 27649 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual024.html -rw-r--r-- root/root 22832 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/tactic-index.html -rw-r--r-- root/root 19565 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/Reference-Manual019.html -rw-r--r-- root/root 21133 2012-05-02 07:48 ./usr/share/doc/coq-doc-html/refman/toc.html -rw-r--r-- root/root 143774 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/Tutorial.v.html -rw-r--r-- root/root 226180 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/FAQ.v.html -rw-r--r-- root/root 138004 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/RecTutorial.html -rw-r--r-- root/root 980 2012-05-02 07:49 ./usr/share/doc/coq-doc-html/changelog.Debian.gz -rw-r--r-- root/root 9966 2012-04-06 05:31 ./usr/share/doc/coq-doc-html/copyright drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc-base/ -rw-r--r-- root/root 745 2012-04-06 05:31 ./usr/share/doc-base/coq-rectutorial-html -rw-r--r-- root/root 513 2012-04-06 05:31 ./usr/share/doc-base/coq-manual-html -rw-r--r-- root/root 523 2012-04-06 05:31 ./usr/share/doc-base/coq-faq-html -rw-r--r-- root/root 515 2012-04-06 05:31 ./usr/share/doc-base/coq-tutorial-html chroot-autobuild/build/buildd/coq-doc-pdf_8.3pl4-1_all.deb: drwxr-xr-x root/root 0 2012-05-02 07:49 ./ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/ drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc/coq-doc-pdf/ -rw-r--r-- root/root 196389 2012-05-02 07:49 ./usr/share/doc/coq-doc-pdf/Tutorial.v.pdf.gz -rw-r--r-- root/root 316137 2012-05-02 07:49 ./usr/share/doc/coq-doc-pdf/RecTutorial.pdf.gz -rw-r--r-- root/root 382678 2012-05-02 07:49 ./usr/share/doc/coq-doc-pdf/FAQ.v.pdf.gz -rw-r--r-- root/root 980 2012-05-02 07:49 ./usr/share/doc/coq-doc-pdf/changelog.Debian.gz -rw-r--r-- root/root 1470932 2012-05-02 07:48 ./usr/share/doc/coq-doc-pdf/Reference-Manual.pdf.gz -rw-r--r-- root/root 9966 2012-04-06 05:31 ./usr/share/doc/coq-doc-pdf/copyright drwxr-xr-x root/root 0 2012-05-02 07:49 ./usr/share/doc-base/ -rw-r--r-- root/root 461 2012-04-06 05:31 ./usr/share/doc-base/coq-tutorial-pdf -rw-r--r-- root/root 690 2012-04-06 05:31 ./usr/share/doc-base/coq-rectutorial-pdf -rw-r--r-- root/root 474 2012-04-06 05:31 ./usr/share/doc-base/coq-faq-pdf -rw-r--r-- root/root 465 2012-04-06 05:31 ./usr/share/doc-base/coq-manual-pdf coq-doc_8.3pl4-1_i386.changes: Format: 1.8 Date: Fri, 06 Apr 2012 07:33:19 +0200 Source: coq-doc Binary: coq-doc coq-doc-html coq-doc-pdf Architecture: all Version: 8.3pl4-1 Distribution: quantal Urgency: low Maintainer: Ubuntu/amd64 Build Daemon Changed-By: Stéphane Glondu Description: coq-doc - documentation for Coq coq-doc-html - documentation for Coq in html format coq-doc-pdf - documentation for Coq in pdf format Changes: coq-doc (8.3pl4-1) unstable; urgency=low . * New upstream release Checksums-Sha1: b45539f6d1ac6060415540693e1f5896da2b3527 4578 coq-doc_8.3pl4-1_all.deb 679755b25bf432438d67a8fe31a622f54b131dff 505154 coq-doc-html_8.3pl4-1_all.deb 81fc3ca24bde0b0f05d63920295ba0197fe74331 2374790 coq-doc-pdf_8.3pl4-1_all.deb Checksums-Sha256: b7ab84386e745beca624e79b9262468d51018a48f29a35f431758ca390be2d97 4578 coq-doc_8.3pl4-1_all.deb 4227dccc0e8dc25fcdaea69e58ec404d6d4b6a283ed285622e04259ad3025991 505154 coq-doc-html_8.3pl4-1_all.deb 28cb6f5b4e2b7a4beb4e0b38eefe0904347aa32334f351e5c91dcc3102f32f8a 2374790 coq-doc-pdf_8.3pl4-1_all.deb Files: 6f86578df557c1b1083f44ea9a56c5c0 4578 non-free/doc optional coq-doc_8.3pl4-1_all.deb 69832829e88c58748c91b8dc60ecf3aa 505154 non-free/doc optional coq-doc-html_8.3pl4-1_all.deb 9d25161ca2c26e822fbc525f22ce9edb 2374790 non-free/doc optional coq-doc-pdf_8.3pl4-1_all.deb ****************************************************************************** Built successfully NOTE: The package could have used binaries from the following packages (access time changed) without a source dependency: tetex-bin: /usr/bin/dvips ****************************************************************************** Finished at 20120502-0749 Build needed 00:15:13, 219884k disk space RUN: /usr/share/launchpad-buildd/slavebin/scan-for-processes ['/usr/share/launchpad-buildd/slavebin/scan-for-processes', '9c515e1d21eaaf895970634411847f687b65d982'] Scanning for processes to kill in build /home/buildd/build-9c515e1d21eaaf895970634411847f687b65d982/chroot-autobuild... RUN: /usr/share/launchpad-buildd/slavebin/umount-chroot ['umount-chroot', '9c515e1d21eaaf895970634411847f687b65d982'] Unmounting chroot for build 9c515e1d21eaaf895970634411847f687b65d982... RUN: /usr/share/launchpad-buildd/slavebin/remove-build ['remove-build', '9c515e1d21eaaf895970634411847f687b65d982'] Removing build 9c515e1d21eaaf895970634411847f687b65d982