>>> Building on localhost under math/coq
BDEPENDS = [shells/bash;sysutils/findlib;devel/gmake;math/ocamlnum;x11/lablgtk3;lang/ocaml]
DIST = [math/coq:coq8.12.0.tar.gz]
FULLPKGNAME = coq8.12.0
RDEPENDS = [lang/ocaml;x11/lablgtk3]
(Junk lock obtained for localhost at 1600006392.86)
>>> Running depends in math/coq at 1600006392.97
last junk was in x11/xfce4/garcon
/usr/sbin/pkg_add aI Drepair bash5.0.18 findlib1.8.1p2 lablgtk33.1.0 ocaml4.10.0 ocamlnum1.1p2
was: /usr/sbin/pkg_add aI Drepair bash5.0.18 findlib1.8.1p2 gmake4.3 lablgtk33.1.0 ocaml4.10.0 ocamlnum1.1p2
/usr/sbin/pkg_add aI Drepair bash5.0.18 findlib1.8.1p2 lablgtk33.1.0 ocaml4.10.0 ocamlnum1.1p2
>>> Running showprepareresults in math/coq at 1600006419.00
===> math/coq
===> coq8.12.0 depends on: lablgtk3* > lablgtk33.1.0
===> coq8.12.0 depends on: ocamlnum* > ocamlnum1.1p2
===> coq8.12.0 depends on: bash* > bash5.0.18
===> coq8.12.0 depends on: findlib* > findlib1.8.1p2
===> coq8.12.0 depends on: ocaml=4.10.0 > ocaml4.10.0
===> coq8.12.0 depends on: gmake* > gmake4.3
===> Verifying specs: atk1.0 c cairo cairogobject fontconfig freetype gdk3 gdk_pixbuf2.0 gio2.0 glib2.0 gobject2.0 gtk3 gtksourceview3.0 harfbuzz intl m pango1.0 pangocairo1.0 pthread z
===> found atk1.0.21809.4 c.96.0 cairo.13.0 cairogobject.2.0 fontconfig.13.0 freetype.30.0 gdk3.2201.1 gdk_pixbuf2.0.3200.2 gio2.0.4200.11 glib2.0.4201.4 gobject2.0.4200.11 gtk3.2201.0 gtksourceview3.0.3.5 harfbuzz.15.4 intl.7.0 m.10.1 pango1.0.3801.1 pangocairo1.0.3801.1 pthread.26.1 z.5.0
bash5.0.18
findlib1.8.1p2
gmake4.3
lablgtk33.1.0
ocaml4.10.0
ocamlnum1.1p2
(Junk lock released for localhost at 1600006421.22)
Woken up x11/kde/i18n3/tg
distfiles size=6774001
>>> Running patch in math/coq at 1600006421.33
===> math/coq
===> Checking files for coq8.12.0
`/usr/ports/distfiles/coq8.12.0.tar.gz' is up to date.
>> (SHA256) coq8.12.0.tar.gz: OK
===> Extracting for coq8.12.0
===> Patching for coq8.12.0
===> Applying OpenBSD patch patchMakefile_ide
Hmm... Looks like a unified diff to me...
The text leading up to this was:

$OpenBSD: patchMakefile_ide,v 1.3 2020/07/16 02:50:08 daniel Exp $

Index: Makefile.ide
 Makefile.ide.orig
+++ Makefile.ide

Patching file Makefile.ide using Plan A...
Hunk #1 succeeded at 187.
done
===> Compiler link: clang > /usr/bin/clang
===> Compiler link: clang++ > /usr/bin/clang++
===> Compiler link: cc > /usr/bin/cc
===> Compiler link: c++ > /usr/bin/c++
>>> Running configure in math/coq at 1600006423.47
===> math/coq
===> Generating configure for coq8.12.0
===> Configuring for coq8.12.0
You have OCaml 4.10.0. Good!
You have OCamlfind 1.8.1. Good!
Warning: Cannot find the OCaml nativecode compiler.
Only the bytecode version of Coq will be available.
You have the Num library installed. Good!
LablGtk3 and LablGtkSourceView3 found ([unspecified]), but no native compiler:
=> only bytecode CoqIde will be built.
Architecture : OpenBSD
Sys.os_type : Unix
Coq VM bytecode link flags : dllib lcoqrun dllpath /usr/local/lib/ocaml/coq/kernel/byterun
Other bytecode link flags :
OCaml version : 4.10.0
OCaml binaries in : /usr/local/bin/
OCaml library in : /usr/local/lib/ocaml
OCaml flambda flags :
Lablgtk3 library in : +lablgtk3sourceview3
CoqIde : byte
Documentation : None
Web browser : firefox remote "OpenURL(%s,newtab)"  firefox %s &
Coq web site : http://coq.inria.fr/
Bytecode VM enabled : true
Native Compiler enabled : true
Paths for true installation:
 the Coq binaries will be copied in /usr/local/bin
 the Coq library will be copied in /usr/local/lib/ocaml/coq
 the Coqide configuration files will be copied in /etc/xdg/coq
 the Coqide data files will be copied in /usr/local/share/coq
 the Coq man pages will be copied in /usr/local/man
 the Coq documentation will be copied in /usr/local/share/doc/coq
 the Coqdoc LaTeX files will be copied in /usr/local/share/texmf/tex/latex/misc
If anything is wrong above, please restart './configure'.
*Warning* To compile the system for a new architecture
don't forget to do a 'make clean' before './configure'.
>>> Running build in math/coq at 1600006426.37
===> math/coq
===> Building for coq8.12.0
ulimit Ss 8192 && cd /usr/obj/ports/coq8.12.0/coq8.12.0 && env i OCAMLFIND_DESTDIR=/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml OCAMLFIND_COMMANDS="ocamldoc=ocamldoc" PORTSDIR="/usr/ports" LIBTOOL="/usr/bin/libtool" PATH='/usr/obj/ports/coq8.12.0/bin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin:/usr/X11R6/bin' PREFIX='/usr/local' LOCALBASE='/usr/local' X11BASE='/usr/X11R6' CFLAGS='O2 pipe' TRUEPREFIX='/usr/local' COQINSTALLPREFIX='' HOME='/coq8.12.0_writes_to_HOME' PICFLAG="fpic" BINGRP=bin BINOWN=root BINMODE=755 NONBINMODE=644 DIRMODE=755 INSTALL_COPY=c INSTALL_STRIP=s MANGRP=bin MANOWN=root MANMODE=644 BSD_INSTALL_PROGRAM="/usr/obj/ports/coq8.12.0/bin/install c s m 755" BSD_INSTALL_SCRIPT="/usr/obj/ports/coq8.12.0/bin/install c m 755" BSD_INSTALL_DATA="/usr/obj/ports/coq8.12.0/bin/install c m 644" BSD_INSTALL_MAN="/usr/obj/ports/coq8.12.0/bin/install c m 644" BSD_INSTALL_PROGRAM_DIR="/usr/obj/ports/coq8.12.0/bin/install d m 755" BSD_INSTALL_SCRIPT_DIR="/usr/obj/ports/coq8.12.0/bin/install d m 755" BSD_INSTALL_DATA_DIR="/usr/obj/ports/coq8.12.0/bin/install d m 755" BSD_INSTALL_MAN_DIR="/usr/obj/ports/coq8.12.0/bin/install d m 755" gmake LIBTOOL="/usr/bin/libtool" SHARED_LIBS_LOG=/usr/obj/ports/coq8.12.0/coq8.12.0/shared_libs.log f Makefile byte coq documentation bin/coqide coqidefiles theories/Init/Prelude.vo
rm f
cp a ".merlin.in" ".merlin"
cp a "ide/.merlin.in" "ide/.merlin"
cp a "kernel/.merlin.in" "kernel/.merlin"
cp a "plugins/.merlin.in" "plugins/.merlin"
cp a "testsuite/unittests/.merlin.in" "testsuite/unittests/.merlin"
cp a "META.coq.in" "META.coq"
mkdir bin
gmake warnundefinedvariable nobuiltinrules f Makefile.build byte coq documentation bin/coqide coqidefiles theories/Init/Prelude.vo
gmake[1]: Entering directory '/usr/obj/ports/coq8.12.0/coq8.12.0'
OCAMLC clib/segmenttree.mli
OCAMLC clib/segmenttree.ml
OCAMLC clib/unicodetable.ml
OCAMLC clib/unicode.mli
OCAMLC clib/unicode.ml
OCAMLC clib/minisys.ml
OCAMLC tools/coqdep_lexer.mli
OCAMLLEX tools/coqdep_lexer.mll
217 states, 2223 transitions, table size 10194 bytes
OCAMLC tools/coqdep_lexer.ml
OCAMLC tools/coqdep_common.mli
OCAMLC tools/coqdep_common.ml
OCAMLC tools/coqdep_boot.ml
OCAMLBEST o bin/coqdep_boot
COQDEP VFILES
OCAMLC kernel/genOpcodeFiles.ml
WRITE kernel/byterun/coq_instruct.h
WRITE kernel/byterun/coq_jumptbl.h
CCDEP kernel/byterun/coq_values.c
CCDEP kernel/byterun/coq_memory.c
CCDEP kernel/byterun/coq_interp.c
CCDEP kernel/byterun/coq_fix_code.c
OCAMLLEX tools/ocamllibdep.mll
14 states, 417 transitions, table size 1752 bytes
OCAMLC tools/ocamllibdep.ml
OCAMLBEST o bin/ocamllibdep
OCAMLC coqpp/coqpp_ast.mli
OCAMLYACC coqpp/coqpp_parse.mly
gmake[1]: Circular coqpp/coqpp_parse.cmi < coqpp/coqpp_parse.cmo dependency dropped.
OCAMLC coqpp/coqpp_parse.mli
OCAMLC coqpp/coqpp_parse.ml
OCAMLLEX coqpp/coqpp_lex.mll
240 states, 15992 transitions, table size 65408 bytes
OCAMLC coqpp/coqpp_lex.ml
OCAMLC a bin/coqpp
mkdir p gramlib/.pack
OCAMLLEX ide/config_lexer.mll
30 states, 1657 transitions, table size 6808 bytes
6052 additional bytes used for bindings
OCAMLLEX ide/coq_lex.mll
118 states, 1659 transitions, table size 7344 bytes
OCAMLLEX ide/protocol/xml_lexer.mll
80 states, 774 transitions, table size 3576 bytes
OCAMLLEX ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX tools/coqdoc/cpretty.mll
2716 states, 8787 transitions, table size 51444 bytes
17625 additional bytes used for bindings
OCAMLLEX tools/coqwc.mll
244 states, 858 transitions, table size 4896 bytes
COQPP parsing/g_constr.mlg
COQPP parsing/g_prim.mlg
COQPP plugins/btauto/g_btauto.mlg
COQPP plugins/cc/g_congruence.mlg
COQPP plugins/derive/g_derive.mlg
COQPP plugins/extraction/g_extraction.mlg
COQPP plugins/firstorder/g_ground.mlg
COQPP plugins/funind/g_indfun.mlg
COQPP plugins/ltac/coretactics.mlg
COQPP plugins/ltac/extraargs.mlg
COQPP plugins/ltac/extratactics.mlg
COQPP plugins/ltac/g_auto.mlg
COQPP plugins/ltac/g_class.mlg
COQPP plugins/ltac/g_eqdecide.mlg
COQPP plugins/ltac/g_ltac.mlg
COQPP plugins/ltac/g_obligations.mlg
COQPP plugins/ltac/g_rewrite.mlg
COQPP plugins/ltac/g_tactic.mlg
COQPP plugins/ltac/profile_ltac_tactics.mlg
COQPP plugins/micromega/g_micromega.mlg
COQPP plugins/micromega/g_zify.mlg
COQPP plugins/nsatz/g_nsatz.mlg
COQPP plugins/omega/g_omega.mlg
COQPP plugins/rtauto/g_rtauto.mlg
COQPP plugins/setoid_ring/g_newring.mlg
COQPP plugins/ssr/ssrparser.mlg
COQPP plugins/ssr/ssrvernac.mlg
COQPP plugins/ssrmatching/g_ssrmatching.mlg
COQPP plugins/ssrsearch/g_search.mlg
COQPP plugins/syntax/g_numeral.mlg
COQPP plugins/syntax/g_string.mlg
COQPP toplevel/g_toplevel.mlg
COQPP vernac/g_proofs.mlg
COQPP vernac/g_vernac.mlg
COQPP usercontrib/Ltac2/g_ltac2.mlg
printf '# 1 "%s"\n' gramlib/ploc.ml > gramlib/.pack/gramlib__Ploc.ml
cat gramlib/ploc.ml >> gramlib/.pack/gramlib__Ploc.ml
printf '# 1 "%s"\n' gramlib/plexing.ml > gramlib/.pack/gramlib__Plexing.ml
cat gramlib/plexing.ml >> gramlib/.pack/gramlib__Plexing.ml
printf '# 1 "%s"\n' gramlib/gramext.ml > gramlib/.pack/gramlib__Gramext.ml
cat gramlib/gramext.ml >> gramlib/.pack/gramlib__Gramext.ml
printf '# 1 "%s"\n' gramlib/grammar.ml > gramlib/.pack/gramlib__Grammar.ml
cat gramlib/grammar.ml >> gramlib/.pack/gramlib__Grammar.ml
echo " \
module Ploc = Gramlib__Ploc \
module Plexing = Gramlib__Plexing \
module Gramext = Gramlib__Gramext \
module Grammar = Gramlib__Grammar" > gramlib/.pack/gramlib.ml
rm f ide/coqide_os_specific.ml && cp ide/coqide_X11.ml.in ide/coqide_os_specific.ml && chmod aw ide/coqide_os_specific.ml
WRITE kernel/copcodes.ml
rm f kernel/uint63.ml && cp kernel/uint63_63.ml kernel/uint63.ml && chmod aw kernel/uint63.ml
printf '# 1 "%s"\n' gramlib/ploc.mli > gramlib/.pack/gramlib__Ploc.mli
cat gramlib/ploc.mli >> gramlib/.pack/gramlib__Ploc.mli
printf '# 1 "%s"\n' gramlib/plexing.mli > gramlib/.pack/gramlib__Plexing.mli
cat gramlib/plexing.mli >> gramlib/.pack/gramlib__Plexing.mli
printf '# 1 "%s"\n' gramlib/gramext.mli > gramlib/.pack/gramlib__Gramext.mli
cat gramlib/gramext.mli >> gramlib/.pack/gramlib__Gramext.mli
printf '# 1 "%s"\n' gramlib/grammar.mli > gramlib/.pack/gramlib__Grammar.mli
cat gramlib/grammar.mli >> gramlib/.pack/gramlib__Grammar.mli
OCAMLLIBDEP usercontrib/MLLIBFILES usercontrib/MLPACKFILES
OCAMLDEP usercontrib/MLFILES usercontrib/MLIFILES
OCAMLLIBDEP plugins/MLLIBFILES plugins/MLPACKFILES
OCAMLDEP plugins/MLFILES plugins/MLIFILES
OCAMLLIBDEP MLLIBFILES MLPACKFILES
OCAMLDEP MLFILES MLIFILES
OCAMLLIBDEP checker/MLLIBFILES checker/MLPACKFILES
OCAMLDEP checker/MLFILES checker/MLIFILES
gmake[1]: Circular coqpp/coqpp_parse.cmi < coqpp/coqpp_parse.cmo dependency dropped.
OCAMLC config/coq_config.mli
OCAMLC config/coq_config.ml
OCAMLC a o config/config.cma
OCAMLC clib/cObj.mli
OCAMLC clib/cObj.ml
OCAMLC clib/cEphemeron.mli
OCAMLC clib/cEphemeron.ml
OCAMLC clib/cSig.mli
OCAMLC clib/cMap.mli
OCAMLC clib/int.mli
OCAMLC clib/hashset.mli
OCAMLC clib/hashset.ml
OCAMLC clib/hashcons.mli
OCAMLC clib/hashcons.ml
OCAMLC clib/orderedType.mli
OCAMLC clib/orderedType.ml
OCAMLC clib/cSet.mli
OCAMLC clib/cSet.ml
OCAMLC clib/cMap.ml
OCAMLC clib/cList.mli
OCAMLC clib/cList.ml
OCAMLC clib/cString.mli
OCAMLC clib/cString.ml
OCAMLC clib/int.ml
OCAMLC clib/range.mli
OCAMLC clib/range.ml
OCAMLC clib/hMap.mli
OCAMLC clib/hMap.ml
OCAMLC clib/bigint.mli
OCAMLC clib/bigint.ml
OCAMLC clib/cArray.mli
OCAMLC clib/cArray.ml
OCAMLC clib/option.mli
OCAMLC clib/option.ml
OCAMLC clib/cUnix.mli
OCAMLC clib/cUnix.ml
OCAMLC clib/cThread.mli
OCAMLC clib/cThread.ml
OCAMLC clib/trie.mli
OCAMLC clib/trie.ml
OCAMLC clib/predicate.mli
OCAMLC clib/predicate.ml
OCAMLC clib/heap.mli
OCAMLC clib/heap.ml
OCAMLC clib/unionfind.mli
OCAMLC clib/unionfind.ml
OCAMLC clib/dyn.mli
OCAMLC clib/dyn.ml
OCAMLC clib/store.mli
OCAMLC clib/store.ml
OCAMLC clib/exninfo.mli
OCAMLC clib/exninfo.ml
OCAMLC clib/iStream.mli
OCAMLC clib/iStream.ml
OCAMLC clib/terminal.mli
OCAMLC clib/terminal.ml
OCAMLC clib/monad.mli
OCAMLC clib/monad.ml
OCAMLC clib/diff2.mli
OCAMLC clib/diff2.ml
OCAMLC a o clib/clib.cma
OCAMLC lib/hook.mli
OCAMLC lib/hook.ml
OCAMLC lib/flags.mli
OCAMLC lib/flags.ml
OCAMLC lib/control.mli
OCAMLC lib/control.ml
OCAMLC lib/util.mli
OCAMLC lib/util.ml
OCAMLC lib/pp.mli
OCAMLC lib/pp.ml
OCAMLC lib/pp_diff.mli
OCAMLC lib/pp_diff.ml
OCAMLC lib/loc.mli
OCAMLC lib/stateid.mli
OCAMLC lib/stateid.ml
OCAMLC lib/loc.ml
OCAMLC lib/xml_datatype.mli
OCAMLC lib/feedback.mli
OCAMLC lib/feedback.ml
OCAMLC lib/cErrors.mli
OCAMLC lib/cErrors.ml
OCAMLC lib/cWarnings.mli
OCAMLC lib/cWarnings.ml
OCAMLC lib/acyclicGraph.mli
OCAMLC lib/acyclicGraph.ml
OCAMLC lib/rtree.mli
OCAMLC lib/rtree.ml
OCAMLC lib/system.mli
OCAMLC lib/system.ml
OCAMLC lib/objFile.mli
OCAMLC lib/objFile.ml
OCAMLC lib/explore.mli
OCAMLC lib/explore.ml
OCAMLC lib/cProfile.mli
OCAMLC lib/cProfile.ml
OCAMLC lib/future.mli
OCAMLC lib/future.ml
OCAMLC lib/spawn.mli
OCAMLC lib/spawn.ml
OCAMLC lib/cAst.mli
OCAMLC lib/cAst.ml
OCAMLC lib/dAst.mli
OCAMLC lib/dAst.ml
OCAMLC lib/genarg.mli
OCAMLC lib/genarg.ml
OCAMLC lib/remoteCounter.mli
OCAMLC lib/remoteCounter.ml
OCAMLC lib/aux_file.mli
OCAMLC lib/aux_file.ml
OCAMLC lib/envars.mli
OCAMLC lib/envars.ml
OCAMLC lib/coqProject_file.mli
OCAMLC lib/coqProject_file.ml
OCAMLC a o lib/lib.cma
OCAMLC kernel/names.mli
OCAMLC kernel/names.ml
OCAMLC kernel/transparentState.mli
OCAMLC kernel/transparentState.ml
OCAMLC kernel/uint63.mli
OCAMLC kernel/uint63.ml
OCAMLC kernel/float64.mli
OCAMLC kernel/float64.ml
OCAMLC kernel/cPrimitives.mli
OCAMLC kernel/cPrimitives.ml
OCAMLC kernel/univ.mli
OCAMLC kernel/univ.ml
OCAMLC kernel/uGraph.mli
OCAMLC kernel/uGraph.ml
OCAMLC kernel/esubst.mli
OCAMLC kernel/esubst.ml
OCAMLC kernel/sorts.mli
OCAMLC kernel/sorts.ml
OCAMLC kernel/evar.mli
OCAMLC kernel/evar.ml
OCAMLC kernel/context.mli
OCAMLC kernel/context.ml
OCAMLC kernel/constr.mli
OCAMLC kernel/constr.ml
OCAMLC kernel/vars.mli
OCAMLC kernel/vars.ml
OCAMLC kernel/term.mli
OCAMLC kernel/term.ml
OCAMLC kernel/retroknowledge.mli
OCAMLC kernel/mod_subst.mli
OCAMLC kernel/mod_subst.ml
OCAMLC kernel/vmvalues.mli
OCAMLC kernel/vmvalues.ml
OCAMLC kernel/cbytecodes.mli
OCAMLC kernel/cbytecodes.ml
OCAMLC kernel/copcodes.ml
OCAMLC kernel/cemitcodes.mli
OCAMLC kernel/cemitcodes.ml
OCAMLC kernel/opaqueproof.mli
OCAMLC kernel/opaqueproof.ml
OCAMLC kernel/conv_oracle.mli
OCAMLC kernel/declarations.ml
OCAMLC kernel/entries.ml
OCAMLC kernel/nativevalues.mli
OCAMLC kernel/nativevalues.ml
OCAMLC kernel/declareops.mli
OCAMLC kernel/declareops.ml
OCAMLC kernel/retroknowledge.ml
OCAMLC kernel/conv_oracle.ml
OCAMLC kernel/environ.mli
OCAMLC kernel/environ.ml
OCAMLC kernel/primred.mli
OCAMLC kernel/primred.ml
OCAMLC kernel/cClosure.mli
OCAMLC kernel/cClosure.ml
OCAMLC kernel/relevanceops.mli
OCAMLC kernel/relevanceops.ml
OCAMLC kernel/reduction.mli
OCAMLC kernel/reduction.ml
OCAMLC kernel/clambda.mli
OCAMLC kernel/clambda.ml
OCAMLC kernel/nativelambda.mli
OCAMLC kernel/nativelambda.ml
OCAMLC kernel/cbytegen.mli
OCAMLC kernel/cbytegen.ml
OCAMLC kernel/nativecode.mli
OCAMLC kernel/nativecode.ml
OCAMLC kernel/nativelib.mli
OCAMLC kernel/nativelib.ml
OCAMLC kernel/csymtable.mli
OCAMLC kernel/csymtable.ml
OCAMLC kernel/vm.mli
OCAMLC kernel/vm.ml
OCAMLC kernel/vconv.mli
OCAMLC kernel/vconv.ml
OCAMLC kernel/nativeconv.mli
OCAMLC kernel/nativeconv.ml
OCAMLC kernel/type_errors.mli
OCAMLC kernel/type_errors.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/inferCumulativity.mli
OCAMLC kernel/inferCumulativity.ml
OCAMLC kernel/indTyping.mli
OCAMLC kernel/indTyping.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/nativelibrary.mli
OCAMLC kernel/nativelibrary.ml
OCAMLC kernel/section.mli
OCAMLC kernel/section.ml
OCAMLC kernel/safe_typing.mli
OCAMLC kernel/safe_typing.ml
OCAMLC a o kernel/kernel.cma
OCAMLC library/libnames.mli
OCAMLC library/libnames.ml
OCAMLC library/globnames.mli
OCAMLC library/globnames.ml
OCAMLC library/libobject.mli
OCAMLC library/libobject.ml
OCAMLC library/summary.mli
OCAMLC library/summary.ml
OCAMLC library/nametab.mli
OCAMLC library/nametab.ml
OCAMLC library/global.mli
OCAMLC library/global.ml
OCAMLC library/lib.mli
OCAMLC library/lib.ml
OCAMLC library/states.mli
OCAMLC library/states.ml
OCAMLC library/goptions.mli
OCAMLC library/goptions.ml
OCAMLC library/coqlib.mli
OCAMLC library/coqlib.ml
OCAMLC a o library/library.cma
OCAMLC engine/univNames.mli
OCAMLC engine/univNames.ml
OCAMLC engine/univGen.mli
OCAMLC engine/univGen.ml
OCAMLC engine/univSubst.mli
OCAMLC engine/univSubst.ml
OCAMLC engine/univProblem.mli
OCAMLC engine/univProblem.ml
OCAMLC engine/univMinim.mli
OCAMLC engine/univMinim.ml
OCAMLC engine/uState.mli
OCAMLC engine/uState.ml
OCAMLC engine/univops.mli
OCAMLC engine/univops.ml
OCAMLC engine/nameops.mli
OCAMLC engine/nameops.ml
OCAMLC engine/evar_kinds.mli
OCAMLC engine/evar_kinds.ml
OCAMLC engine/evd.mli
OCAMLC engine/evd.ml
OCAMLC engine/eConstr.mli
OCAMLC engine/eConstr.ml
OCAMLC engine/namegen.mli
OCAMLC engine/namegen.ml
OCAMLC engine/termops.mli
OCAMLC engine/termops.ml
OCAMLC engine/evarutil.mli
OCAMLC engine/evarutil.ml
OCAMLC engine/logic_monad.mli
OCAMLC engine/logic_monad.ml
OCAMLC engine/proofview_monad.mli
OCAMLC engine/proofview_monad.ml
OCAMLC engine/proofview.mli
OCAMLC engine/proofview.ml
OCAMLC engine/ftactic.mli
OCAMLC engine/ftactic.ml
OCAMLC a o engine/engine.cma
OCAMLC pretyping/geninterp.mli
OCAMLC pretyping/geninterp.ml
OCAMLC pretyping/locus.ml
OCAMLC pretyping/locusops.mli
OCAMLC pretyping/locusops.ml
OCAMLC pretyping/pretype_errors.mli
OCAMLC pretyping/pretype_errors.ml
OCAMLC pretyping/reductionops.mli
OCAMLC pretyping/reductionops.ml
OCAMLC pretyping/inductiveops.mli
OCAMLC pretyping/inductiveops.ml
OCAMLC pretyping/arguments_renaming.mli
OCAMLC pretyping/arguments_renaming.ml
OCAMLC pretyping/retyping.mli
OCAMLC pretyping/retyping.ml
OCAMLC pretyping/vnorm.mli
OCAMLC pretyping/vnorm.ml
OCAMLC pretyping/nativenorm.mli
OCAMLC pretyping/nativenorm.ml
OCAMLC pretyping/cbv.mli
OCAMLC pretyping/cbv.ml
OCAMLC pretyping/find_subterm.mli
OCAMLC pretyping/find_subterm.ml
OCAMLC pretyping/evardefine.mli
OCAMLC pretyping/evardefine.ml
OCAMLC pretyping/evarsolve.mli
OCAMLC pretyping/evarsolve.ml
OCAMLC pretyping/recordops.mli
OCAMLC pretyping/recordops.ml
OCAMLC pretyping/heads.mli
OCAMLC pretyping/heads.ml
OCAMLC pretyping/evarconv.mli
OCAMLC pretyping/evarconv.ml
OCAMLC pretyping/typing.mli
OCAMLC pretyping/typing.ml
OCAMLC pretyping/glob_term.ml
OCAMLC pretyping/ltac_pretype.ml
OCAMLC pretyping/glob_ops.mli
OCAMLC pretyping/glob_ops.ml
OCAMLC pretyping/pattern.ml
OCAMLC pretyping/patternops.mli
OCAMLC pretyping/patternops.ml
OCAMLC pretyping/constr_matching.mli
OCAMLC pretyping/constr_matching.ml
OCAMLC pretyping/tacred.mli
OCAMLC pretyping/tacred.ml
OCAMLC pretyping/typeclasses_errors.mli
OCAMLC pretyping/typeclasses_errors.ml
OCAMLC pretyping/typeclasses.mli
OCAMLC pretyping/typeclasses.ml
OCAMLC pretyping/coercionops.mli
OCAMLC pretyping/coercionops.ml
OCAMLC pretyping/program.mli
OCAMLC pretyping/program.ml
OCAMLC pretyping/coercion.mli
OCAMLC pretyping/coercion.ml
OCAMLC pretyping/detyping.mli
OCAMLC pretyping/detyping.ml
OCAMLC pretyping/indrec.mli
OCAMLC pretyping/indrec.ml
OCAMLC pretyping/globEnv.mli
OCAMLC pretyping/globEnv.ml
OCAMLC pretyping/cases.mli
OCAMLC pretyping/cases.ml
OCAMLC pretyping/pretyping.mli
OCAMLC pretyping/pretyping.ml
OCAMLC pretyping/keys.mli
OCAMLC pretyping/keys.ml
OCAMLC pretyping/unification.mli
OCAMLC pretyping/unification.ml
OCAMLC a o pretyping/pretyping.cma
OCAMLC interp/deprecation.mli
OCAMLC interp/deprecation.ml
OCAMLC interp/numTok.mli
OCAMLC interp/numTok.ml
OCAMLC interp/constrexpr.ml
OCAMLC proofs/tactypes.ml
OCAMLC interp/notation_term.ml
OCAMLC interp/genintern.mli
OCAMLC interp/stdarg.mli
OCAMLC interp/stdarg.ml
OCAMLC interp/genintern.ml
OCAMLC interp/notation_ops.mli
OCAMLC interp/notation_ops.ml
OCAMLC interp/notation.mli
OCAMLC interp/notation.ml
OCAMLC interp/syntax_def.mli
OCAMLC interp/syntax_def.ml
OCAMLC interp/smartlocate.mli
OCAMLC interp/smartlocate.ml
OCAMLC interp/constrexpr_ops.mli
OCAMLC interp/constrexpr_ops.ml
OCAMLC interp/decls.mli
OCAMLC interp/decls.ml
OCAMLC interp/dumpglob.mli
OCAMLC interp/dumpglob.ml
OCAMLC interp/reserve.mli
OCAMLC interp/reserve.ml
OCAMLC interp/impargs.mli
OCAMLC interp/impargs.ml
OCAMLC interp/implicit_quantifiers.mli
OCAMLC interp/implicit_quantifiers.ml
OCAMLC interp/constrintern.mli
OCAMLC interp/constrintern.ml
OCAMLC interp/modintern.mli
OCAMLC interp/modintern.ml
OCAMLC interp/constrextern.mli
OCAMLC interp/constrextern.ml
OCAMLC a o interp/interp.cma
OCAMLC proofs/miscprint.mli
OCAMLC proofs/miscprint.ml
OCAMLC proofs/goal.mli
OCAMLC proofs/goal.ml
OCAMLC proofs/evar_refiner.mli
OCAMLC proofs/evar_refiner.ml
OCAMLC proofs/refine.mli
OCAMLC proofs/refine.ml
OCAMLC proofs/goal_select.mli
OCAMLC proofs/proof.mli
OCAMLC proofs/proof.ml
OCAMLC proofs/logic.mli
OCAMLC proofs/logic.ml
OCAMLC proofs/goal_select.ml
OCAMLC proofs/proof_bullet.mli
OCAMLC proofs/proof_bullet.ml
OCAMLC proofs/refiner.mli
OCAMLC proofs/refiner.ml
OCAMLC proofs/tacmach.mli
OCAMLC proofs/tacmach.ml
OCAMLC proofs/clenv.mli
OCAMLC proofs/clenv.ml
OCAMLC proofs/clenvtac.mli
OCAMLC proofs/clenvtac.ml
OCAMLC a o proofs/proofs.cma
OCAMLC gramlib/.pack/gramlib.ml
OCAMLC gramlib/.pack/gramlib__Ploc.mli
OCAMLC gramlib/.pack/gramlib__Ploc.ml
OCAMLC gramlib/.pack/gramlib__Plexing.mli
OCAMLC gramlib/.pack/gramlib__Plexing.ml
OCAMLC gramlib/.pack/gramlib__Gramext.mli
OCAMLC gramlib/.pack/gramlib__Gramext.ml
OCAMLC gramlib/.pack/gramlib__Grammar.mli
OCAMLC gramlib/.pack/gramlib__Grammar.ml
OCAMLC a o gramlib/.pack/gramlib.cma
OCAMLC parsing/tok.mli
OCAMLC parsing/tok.ml
OCAMLC parsing/cLexer.mli
OCAMLC parsing/cLexer.ml
OCAMLC parsing/extend.ml
OCAMLC parsing/notation_gram.ml
OCAMLC parsing/notgram_ops.mli
OCAMLC parsing/notgram_ops.ml
OCAMLC parsing/ppextend.mli
OCAMLC parsing/ppextend.ml
OCAMLC parsing/pcoq.mli
OCAMLC parsing/pcoq.ml
OCAMLC parsing/g_constr.ml
OCAMLC parsing/g_prim.ml
OCAMLC a o parsing/parsing.cma
OCAMLC printing/genprint.mli
OCAMLC printing/genprint.ml
OCAMLC printing/pputils.mli
OCAMLC printing/pputils.ml
OCAMLC printing/ppconstr.mli
OCAMLC printing/ppconstr.ml
OCAMLC printing/proof_diffs.mli
OCAMLC printing/proof_diffs.ml
OCAMLC printing/printer.mli
OCAMLC printing/printer.ml
OCAMLC printing/printmod.mli
OCAMLC printing/printmod.ml
OCAMLC a o printing/printing.cma
OCAMLC tactics/declareScheme.mli
OCAMLC tactics/declareScheme.ml
OCAMLC tactics/dnet.mli
OCAMLC tactics/dnet.ml
OCAMLC tactics/dn.mli
OCAMLC tactics/dn.ml
OCAMLC tactics/btermdn.mli
OCAMLC tactics/btermdn.ml
OCAMLC tactics/tacticals.mli
OCAMLC tactics/tacticals.ml
OCAMLC tactics/hipattern.mli
OCAMLC tactics/hipattern.ml
OCAMLC tactics/ind_tables.mli
OCAMLC tactics/ind_tables.ml
OCAMLC tactics/eqschemes.mli
OCAMLC tactics/eqschemes.ml
OCAMLC tactics/elimschemes.mli
OCAMLC tactics/elimschemes.ml
OCAMLC tactics/genredexpr.ml
OCAMLC tactics/redops.mli
OCAMLC tactics/redops.ml
OCAMLC tactics/redexpr.mli
OCAMLC tactics/redexpr.ml
OCAMLC tactics/ppred.mli
OCAMLC tactics/ppred.ml
OCAMLC tactics/tactics.mli
OCAMLC tactics/tactics.ml
OCAMLC tactics/abstract.mli
OCAMLC tactics/abstract.ml
OCAMLC tactics/elim.mli
OCAMLC tactics/elim.ml
OCAMLC tactics/equality.mli
OCAMLC tactics/equality.ml
OCAMLC tactics/contradiction.mli
OCAMLC tactics/contradiction.ml
OCAMLC tactics/inv.mli
OCAMLC tactics/inv.ml
OCAMLC tactics/declareUctx.mli
OCAMLC tactics/declareUctx.ml
OCAMLC tactics/hints.mli
OCAMLC tactics/hints.ml
OCAMLC tactics/auto.mli
OCAMLC tactics/auto.ml
OCAMLC tactics/eauto.mli
OCAMLC tactics/eauto.ml
OCAMLC tactics/class_tactics.mli
OCAMLC tactics/class_tactics.ml
OCAMLC tactics/term_dnet.mli
OCAMLC tactics/term_dnet.ml
OCAMLC tactics/eqdecide.mli
OCAMLC tactics/eqdecide.ml
OCAMLC tactics/autorewrite.mli
OCAMLC tactics/autorewrite.ml
OCAMLC a o tactics/tactics.cma
OCAMLC vernac/declaremods.mli
OCAMLC vernac/attributes.mli
OCAMLC vernac/vernacexpr.ml
OCAMLC vernac/attributes.ml
OCAMLC vernac/pvernac.mli
OCAMLC vernac/pvernac.ml
OCAMLC vernac/declaremods.ml
OCAMLC vernac/g_vernac.ml
OCAMLC vernac/retrieveObl.mli
OCAMLC vernac/declare.mli
OCAMLC vernac/g_proofs.ml
OCAMLC vernac/vernacprop.mli
OCAMLC vernac/vernacprop.ml
OCAMLC vernac/himsg.mli
OCAMLC vernac/himsg.ml
OCAMLC vernac/locality.mli
OCAMLC vernac/locality.ml
OCAMLC vernac/egramml.mli
OCAMLC vernac/egramml.ml
OCAMLC vernac/declareObl.mli
OCAMLC vernac/lemmas.mli
OCAMLC vernac/vernacextend.mli
OCAMLC vernac/vernacextend.ml
OCAMLC vernac/ppvernac.mli
OCAMLC vernac/ppvernac.ml
OCAMLC vernac/proof_using.mli
OCAMLC vernac/proof_using.ml
OCAMLC vernac/egramcoq.mli
OCAMLC vernac/egramcoq.ml
OCAMLC vernac/metasyntax.mli
OCAMLC vernac/metasyntax.ml
OCAMLC vernac/declareUniv.mli
OCAMLC vernac/declareUniv.ml
OCAMLC vernac/retrieveObl.ml
OCAMLC vernac/declare.ml
OCAMLC vernac/declareObl.ml
OCAMLC vernac/comHints.mli
OCAMLC vernac/comHints.ml
OCAMLC vernac/canonical.mli
OCAMLC vernac/canonical.ml
OCAMLC vernac/recLemmas.mli
OCAMLC vernac/recLemmas.ml
OCAMLC vernac/library.mli
OCAMLC vernac/library.ml
OCAMLC vernac/lemmas.ml
OCAMLC vernac/comCoercion.mli
OCAMLC vernac/comCoercion.ml
OCAMLC vernac/auto_ind_decl.mli
OCAMLC vernac/auto_ind_decl.ml
OCAMLC vernac/indschemes.mli
OCAMLC vernac/indschemes.ml
OCAMLC vernac/obligations.mli
OCAMLC vernac/obligations.ml
OCAMLC vernac/comDefinition.mli
OCAMLC vernac/comDefinition.ml
OCAMLC vernac/classes.mli
OCAMLC vernac/classes.ml
OCAMLC vernac/comPrimitive.mli
OCAMLC vernac/comPrimitive.ml
OCAMLC vernac/comAssumption.mli
OCAMLC vernac/comAssumption.ml
OCAMLC vernac/declareInd.mli
OCAMLC vernac/declareInd.ml
OCAMLC vernac/search.mli
OCAMLC vernac/search.ml
OCAMLC vernac/comSearch.mli
OCAMLC vernac/comSearch.ml
OCAMLC vernac/prettyp.mli
OCAMLC vernac/prettyp.ml
OCAMLC vernac/comInductive.mli
OCAMLC vernac/comInductive.ml
OCAMLC vernac/comFixpoint.mli
OCAMLC vernac/comFixpoint.ml
OCAMLC vernac/comProgramFixpoint.mli
OCAMLC vernac/comProgramFixpoint.ml
OCAMLC vernac/record.mli
OCAMLC vernac/record.ml
OCAMLC vernac/assumptions.mli
OCAMLC vernac/assumptions.ml
OCAMLC vernac/mltop.mli
OCAMLC vernac/mltop.ml
OCAMLC vernac/topfmt.mli
OCAMLC vernac/topfmt.ml
OCAMLC vernac/loadpath.mli
OCAMLC vernac/loadpath.ml
OCAMLC vernac/comArguments.mli
OCAMLC vernac/comArguments.ml
OCAMLC vernac/vernacentries.mli
OCAMLC vernac/vernacentries.ml
OCAMLC vernac/vernacstate.mli
OCAMLC vernac/vernacstate.ml
OCAMLC vernac/vernacinterp.mli
OCAMLC vernac/vernacinterp.ml
OCAMLC vernac/proof_global.ml
OCAMLC vernac/pfedit.ml
OCAMLC vernac/declareDef.ml
OCAMLC a o vernac/vernac.cma
OCAMLC stm/spawned.mli
OCAMLC stm/spawned.ml
OCAMLC stm/dag.mli
OCAMLC stm/dag.ml
OCAMLC stm/vcs.mli
OCAMLC stm/vcs.ml
OCAMLC stm/tQueue.mli
OCAMLC stm/tQueue.ml
OCAMLC stm/coqworkmgrApi.mli
OCAMLC stm/workerPool.mli
OCAMLC stm/workerPool.ml
OCAMLC stm/vernac_classifier.mli
OCAMLC stm/vernac_classifier.ml
OCAMLC stm/coqworkmgrApi.ml
OCAMLC stm/asyncTaskQueue.mli
OCAMLC stm/asyncTaskQueue.ml
OCAMLC stm/stm.mli
OCAMLC stm/stm.ml
OCAMLC stm/proofBlockDelimiter.mli
OCAMLC stm/proofBlockDelimiter.ml
OCAMLC stm/vio_checking.mli
OCAMLC stm/vio_checking.ml
OCAMLC a o stm/stm.cma
OCAMLC toplevel/vernac.mli
OCAMLC toplevel/vernac.ml
OCAMLC toplevel/usage.mli
OCAMLC toplevel/usage.ml
OCAMLC toplevel/coqinit.mli
OCAMLC toplevel/coqinit.ml
OCAMLC toplevel/coqargs.mli
OCAMLC toplevel/coqargs.ml
OCAMLC toplevel/coqcargs.mli
OCAMLC toplevel/coqcargs.ml
OCAMLC toplevel/g_toplevel.ml
OCAMLC toplevel/coqloop.mli
OCAMLC toplevel/coqloop.ml
OCAMLC toplevel/ccompile.mli
OCAMLC toplevel/ccompile.ml
OCAMLC toplevel/coqtop.mli
OCAMLC toplevel/coqtop.ml
OCAMLC toplevel/workerLoop.mli
OCAMLC toplevel/workerLoop.ml
OCAMLC toplevel/coqc.mli
OCAMLC toplevel/coqc.ml
OCAMLC a o toplevel/toplevel.cma
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/ && \
"/usr/local/bin/ocamlfind" ocamlmklib oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
COQMKTOP o bin/coqtop.byte
findlib: [WARNING] Interface topdirs.cmi occurs in several directories: /usr/local/lib/ocaml/compilerlibs, /usr/local/lib/ocaml
COQMKTOP o bin/coqproofworker.byte
COQMKTOP o bin/coqtacticworker.byte
COQMKTOP o bin/coqqueryworker.byte
COQMKTOP o bin/coqc.byte
OCAMLC checker/analyze.mli
OCAMLC checker/analyze.ml
OCAMLC checker/checkFlags.mli
OCAMLC checker/checkFlags.ml
OCAMLC checker/checkInductive.mli
OCAMLC checker/checkInductive.ml
OCAMLC checker/mod_checking.mli
OCAMLC checker/mod_checking.ml
OCAMLC checker/checkTypes.mli
OCAMLC checker/checkTypes.ml
OCAMLC checker/safe_checking.mli
OCAMLC checker/safe_checking.ml
OCAMLC checker/values.mli
OCAMLC checker/values.ml
OCAMLC checker/validate.mli
OCAMLC checker/validate.ml
OCAMLC checker/check.mli
OCAMLC checker/check.ml
OCAMLC checker/check_stat.mli
OCAMLC checker/check_stat.ml
OCAMLC checker/checker.mli
OCAMLC checker/checker.ml
OCAMLC a o checker/check.cma
OCAMLC o bin/coqchk.byte
OCAMLC ide/protocol/xml_lexer.mli
OCAMLC ide/protocol/xml_lexer.ml
OCAMLC ide/protocol/xml_parser.mli
OCAMLC ide/protocol/xml_parser.ml
OCAMLC ide/protocol/xml_printer.mli
OCAMLC ide/protocol/xml_printer.ml
OCAMLC ide/protocol/serialize.mli
OCAMLC ide/protocol/serialize.ml
OCAMLC ide/protocol/richpp.mli
OCAMLC ide/protocol/richpp.ml
OCAMLC ide/protocol/interface.ml
OCAMLC ide/protocol/xmlprotocol.mli
OCAMLC ide/protocol/xmlprotocol.ml
OCAMLC a o ide/protocol/ideprotocol.cma
OCAMLC ide/minilib.mli
OCAMLC ide/minilib.ml
OCAMLC ide/configwin_messages.ml
OCAMLC ide/configwin_types.ml
OCAMLC ide/configwin_ihm.mli
OCAMLC ide/configwin_ihm.ml
OCAMLC ide/configwin.mli
OCAMLC ide/configwin.ml
OCAMLC ide/tags.mli
OCAMLC ide/tags.ml
OCAMLC ide/wg_Notebook.mli
OCAMLC ide/wg_Notebook.ml
OCAMLC ide/config_lexer.mli
OCAMLC ide/config_lexer.ml
OCAMLC ide/utf8_convert.mli
OCAMLC ide/utf8_convert.ml
OCAMLC ide/preferences.mli
OCAMLC ide/preferences.ml
OCAMLC ide/ideutils.mli
OCAMLC ide/ideutils.ml
OCAMLC ide/unicode_bindings.mli
OCAMLC ide/unicode_bindings.ml
OCAMLC ide/coq.mli
OCAMLC ide/coq.ml
OCAMLC ide/coq_lex.mli
OCAMLC ide/coq_lex.ml
OCAMLC ide/sentence.mli
OCAMLC ide/sentence.ml
OCAMLC ide/gtk_parsing.mli
OCAMLC ide/gtk_parsing.ml
OCAMLC ide/wg_Segment.mli
OCAMLC ide/wg_Segment.ml
OCAMLC ide/wg_ProofView.mli
OCAMLC ide/wg_ProofView.ml
OCAMLC ide/wg_MessageView.mli
OCAMLC ide/wg_MessageView.ml
OCAMLC ide/wg_RoutedMessageViews.mli
OCAMLC ide/wg_RoutedMessageViews.ml
OCAMLC ide/wg_Detachable.mli
OCAMLC ide/wg_Detachable.ml
OCAMLC ide/wg_Find.mli
OCAMLC ide/wg_Find.ml
OCAMLC ide/wg_Completion.mli
OCAMLC ide/wg_Completion.ml
OCAMLC ide/wg_ScriptView.mli
OCAMLC ide/wg_ScriptView.ml
OCAMLC ide/coq_commands.mli
OCAMLC ide/coq_commands.ml
OCAMLC ide/fileOps.mli
OCAMLC ide/fileOps.ml
OCAMLC ide/document.mli
OCAMLC ide/document.ml
OCAMLC ide/coqOps.mli
OCAMLC ide/coqOps.ml
OCAMLC ide/wg_Command.mli
OCAMLC ide/wg_Command.ml
OCAMLC ide/session.mli
OCAMLC ide/session.ml
OCAMLC ide/coqide_ui.mli
OCAMLC ide/coqide_ui.ml
OCAMLC ide/microPG.mli
OCAMLC ide/microPG.ml
OCAMLC ide/coqide.mli
OCAMLC ide/coqide.ml
OCAMLC a o ide/ide.cma
OCAMLC ide/coqide_os_specific.mli
OCAMLC ide/coqide_os_specific.ml
OCAMLC o bin/coqide.byte
OCAMLC a o ide/ide_common.cma
COQMKTOP o bin/coqidetop.byte
OCAMLC plugins/ltac/tacexpr.mli
OCAMLC plugins/ltac/tacexpr.ml
OCAMLC plugins/ltac/tacarg.mli
OCAMLC plugins/ltac/tacarg.ml
OCAMLC plugins/ltac/tacsubst.mli
OCAMLC plugins/ltac/tacsubst.ml
OCAMLC plugins/ltac/tacenv.mli
OCAMLC plugins/ltac/tacenv.ml
OCAMLC plugins/ltac/pptactic.mli
OCAMLC plugins/ltac/pptactic.ml
OCAMLC plugins/ltac/pltac.mli
OCAMLC plugins/ltac/pltac.ml
OCAMLC plugins/ltac/taccoerce.mli
OCAMLC plugins/ltac/taccoerce.ml
OCAMLC plugins/ltac/tactic_debug.mli
OCAMLC plugins/ltac/tactic_debug.ml
OCAMLC plugins/ltac/tacintern.mli
OCAMLC plugins/ltac/tacintern.ml
OCAMLC plugins/ltac/profile_ltac.mli
OCAMLC plugins/ltac/profile_ltac.ml
OCAMLC plugins/ltac/tactic_matching.mli
OCAMLC plugins/ltac/tactic_matching.ml
OCAMLC plugins/ltac/leminv.mli
OCAMLC plugins/ltac/leminv.ml
OCAMLC plugins/ltac/tacinterp.mli
OCAMLC plugins/ltac/tacinterp.ml
OCAMLC plugins/ltac/tacentries.mli
OCAMLC plugins/ltac/tacentries.ml
OCAMLC plugins/ltac/evar_tactics.mli
OCAMLC plugins/ltac/evar_tactics.ml
OCAMLC plugins/ltac/tactic_option.mli
OCAMLC plugins/ltac/tactic_option.ml
OCAMLC plugins/ltac/extraargs.mli
OCAMLC plugins/ltac/extraargs.ml
OCAMLC plugins/ltac/g_obligations.ml
OCAMLC plugins/ltac/coretactics.ml
OCAMLC plugins/ltac/extratactics.mli
OCAMLC plugins/ltac/extratactics.ml
OCAMLC plugins/ltac/profile_ltac_tactics.ml
OCAMLC plugins/ltac/g_auto.ml
OCAMLC plugins/ltac/g_class.ml
OCAMLC plugins/ltac/rewrite.mli
OCAMLC plugins/ltac/rewrite.ml
OCAMLC plugins/ltac/g_rewrite.ml
OCAMLC plugins/ltac/g_eqdecide.ml
OCAMLC plugins/ltac/g_tactic.ml
OCAMLC plugins/ltac/g_ltac.ml
OCAMLC pack o plugins/ltac/ltac_plugin.cmo
OCAMLC plugins/ltac/tauto.mli
OCAMLC plugins/ltac/tauto.ml
OCAMLC pack o plugins/ltac/tauto_plugin.cmo
OCAMLC plugins/omega/omega.ml
OCAMLC plugins/omega/coq_omega.mli
OCAMLC plugins/omega/coq_omega.ml
OCAMLC plugins/omega/g_omega.ml
OCAMLC pack o plugins/omega/omega_plugin.cmo
OCAMLC plugins/micromega/micromega.mli
OCAMLC plugins/micromega/micromega.ml
OCAMLC plugins/micromega/numCompat.mli
OCAMLC plugins/micromega/numCompat.ml
OCAMLC plugins/micromega/mutils.mli
OCAMLC plugins/micromega/mutils.ml
OCAMLC plugins/micromega/itv.mli
OCAMLC plugins/micromega/itv.ml
OCAMLC plugins/micromega/vect.mli
OCAMLC plugins/micromega/vect.ml
OCAMLC plugins/micromega/sos_types.mli
OCAMLC plugins/micromega/sos_types.ml
OCAMLC plugins/micromega/polynomial.mli
OCAMLC plugins/micromega/polynomial.ml
OCAMLC plugins/micromega/mfourier.mli
OCAMLC plugins/micromega/mfourier.ml
OCAMLC plugins/micromega/simplex.mli
OCAMLC plugins/micromega/simplex.ml
OCAMLC plugins/micromega/certificate.mli
OCAMLC plugins/micromega/certificate.ml
OCAMLC plugins/micromega/persistent_cache.mli
OCAMLC plugins/micromega/persistent_cache.ml
OCAMLC plugins/micromega/coq_micromega.mli
OCAMLC plugins/micromega/coq_micromega.ml
OCAMLC plugins/micromega/g_micromega.mli
OCAMLC plugins/micromega/g_micromega.ml
OCAMLC pack o plugins/micromega/micromega_plugin.cmo
OCAMLC plugins/setoid_ring/newring_ast.mli
OCAMLC plugins/setoid_ring/newring_ast.ml
OCAMLC plugins/setoid_ring/newring.mli
OCAMLC plugins/setoid_ring/newring.ml
OCAMLC plugins/setoid_ring/g_newring.ml
OCAMLC pack o plugins/setoid_ring/newring_plugin.cmo
OCAMLC plugins/extraction/miniml.mli
OCAMLC plugins/extraction/miniml.ml
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/json.mli
OCAMLC plugins/extraction/json.ml
OCAMLC plugins/extraction/extract_env.mli
OCAMLC plugins/extraction/extract_env.ml
OCAMLC plugins/extraction/g_extraction.ml
OCAMLC pack o plugins/extraction/extraction_plugin.cmo
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
OCAMLC plugins/cc/g_congruence.ml
OCAMLC pack o plugins/cc/cc_plugin.cmo
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
OCAMLC plugins/firstorder/g_ground.ml
OCAMLC pack o plugins/firstorder/ground_plugin.cmo
OCAMLC plugins/rtauto/proof_search.mli
OCAMLC plugins/rtauto/proof_search.ml
OCAMLC plugins/rtauto/refl_tauto.mli
OCAMLC plugins/rtauto/refl_tauto.ml
OCAMLC plugins/rtauto/g_rtauto.ml
OCAMLC pack o plugins/rtauto/rtauto_plugin.cmo
OCAMLC plugins/btauto/refl_btauto.mli
OCAMLC plugins/btauto/refl_btauto.ml
OCAMLC plugins/btauto/g_btauto.ml
OCAMLC pack o plugins/btauto/btauto_plugin.cmo
OCAMLC plugins/funind/indfun_common.mli
OCAMLC plugins/funind/indfun_common.ml
OCAMLC plugins/funind/glob_termops.mli
OCAMLC plugins/funind/glob_termops.ml
OCAMLC plugins/funind/recdef.mli
OCAMLC plugins/funind/recdef.ml
OCAMLC plugins/funind/glob_term_to_relation.mli
OCAMLC plugins/funind/glob_term_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
OCAMLC plugins/funind/invfun.mli
OCAMLC plugins/funind/invfun.ml
OCAMLC plugins/funind/indfun.mli
OCAMLC plugins/funind/indfun.ml
OCAMLC plugins/funind/gen_principle.mli
OCAMLC plugins/funind/gen_principle.ml
OCAMLC plugins/funind/g_indfun.ml
OCAMLC pack o plugins/funind/recdef_plugin.cmo
OCAMLC plugins/nsatz/utile.mli
OCAMLC plugins/nsatz/utile.ml
OCAMLC plugins/nsatz/polynom.mli
OCAMLC plugins/nsatz/polynom.ml
OCAMLC plugins/nsatz/ideal.mli
OCAMLC plugins/nsatz/ideal.ml
OCAMLC plugins/nsatz/nsatz.mli
OCAMLC plugins/nsatz/nsatz.ml
OCAMLC plugins/nsatz/g_nsatz.ml
OCAMLC pack o plugins/nsatz/nsatz_plugin.cmo
OCAMLC plugins/syntax/r_syntax.mli
OCAMLC plugins/syntax/r_syntax.ml
OCAMLC pack o plugins/syntax/r_syntax_plugin.cmo
OCAMLC plugins/syntax/int63_syntax.ml
OCAMLC pack o plugins/syntax/int63_syntax_plugin.cmo
OCAMLC plugins/syntax/float_syntax.ml
OCAMLC pack o plugins/syntax/float_syntax_plugin.cmo
OCAMLC plugins/syntax/numeral.mli
OCAMLC plugins/syntax/numeral.ml
OCAMLC plugins/syntax/g_numeral.ml
OCAMLC pack o plugins/syntax/numeral_notation_plugin.cmo
OCAMLC plugins/syntax/string_notation.mli
OCAMLC plugins/syntax/string_notation.ml
OCAMLC plugins/syntax/g_string.ml
OCAMLC pack o plugins/syntax/string_notation_plugin.cmo
OCAMLC plugins/derive/derive.mli
OCAMLC plugins/derive/derive.ml
OCAMLC plugins/derive/g_derive.ml
OCAMLC pack o plugins/derive/derive_plugin.cmo
OCAMLC plugins/ssrmatching/ssrmatching.mli
OCAMLC plugins/ssrmatching/ssrmatching.ml
OCAMLC plugins/ssrmatching/g_ssrmatching.mli
OCAMLC plugins/ssrmatching/g_ssrmatching.ml
OCAMLC pack o plugins/ssrmatching/ssrmatching_plugin.cmo
OCAMLC plugins/ssr/ssrast.mli
OCAMLC plugins/ssr/ssrprinters.mli
OCAMLC plugins/ssr/ssrprinters.ml
OCAMLC plugins/ssr/ssrcommon.mli
OCAMLC plugins/ssr/ssrcommon.ml
OCAMLC plugins/ssr/ssrtacticals.mli
OCAMLC plugins/ssr/ssrtacticals.ml
OCAMLC plugins/ssr/ssrelim.mli
OCAMLC plugins/ssr/ssrelim.ml
OCAMLC plugins/ssr/ssrview.mli
OCAMLC plugins/ssr/ssrview.ml
OCAMLC plugins/ssr/ssrbwd.mli
OCAMLC plugins/ssr/ssrbwd.ml
OCAMLC plugins/ssr/ssrequality.mli
OCAMLC plugins/ssr/ssrequality.ml
OCAMLC plugins/ssr/ssripats.mli
OCAMLC plugins/ssr/ssripats.ml
OCAMLC plugins/ssr/ssrfwd.mli
OCAMLC plugins/ssr/ssrfwd.ml
OCAMLC plugins/ssr/ssrparser.mli
OCAMLC plugins/ssr/ssrparser.ml
OCAMLC plugins/ssr/ssrvernac.mli
OCAMLC plugins/ssr/ssrvernac.ml
OCAMLC pack o plugins/ssr/ssreflect_plugin.cmo
OCAMLC plugins/ssrsearch/g_search.ml
OCAMLC pack o plugins/ssrsearch/ssrsearch_plugin.cmo
OCAMLC usercontrib/Ltac2/tac2dyn.mli
OCAMLC usercontrib/Ltac2/tac2dyn.ml
OCAMLC usercontrib/Ltac2/tac2expr.mli
OCAMLC usercontrib/Ltac2/tac2ffi.mli
OCAMLC usercontrib/Ltac2/tac2ffi.ml
OCAMLC usercontrib/Ltac2/tac2env.mli
OCAMLC usercontrib/Ltac2/tac2env.ml
OCAMLC usercontrib/Ltac2/tac2print.mli
OCAMLC usercontrib/Ltac2/tac2print.ml
OCAMLC usercontrib/Ltac2/tac2intern.mli
OCAMLC usercontrib/Ltac2/tac2intern.ml
OCAMLC usercontrib/Ltac2/tac2interp.mli
OCAMLC usercontrib/Ltac2/tac2interp.ml
OCAMLC usercontrib/Ltac2/tac2qexpr.mli
OCAMLC usercontrib/Ltac2/tac2entries.mli
OCAMLC usercontrib/Ltac2/tac2entries.ml
OCAMLC usercontrib/Ltac2/tac2quote.mli
OCAMLC usercontrib/Ltac2/tac2quote.ml
OCAMLC usercontrib/Ltac2/tac2match.mli
OCAMLC usercontrib/Ltac2/tac2match.ml
OCAMLC usercontrib/Ltac2/tac2core.mli
OCAMLC usercontrib/Ltac2/tac2core.ml
OCAMLC usercontrib/Ltac2/tac2types.mli
OCAMLC usercontrib/Ltac2/tac2extffi.mli
OCAMLC usercontrib/Ltac2/tac2extffi.ml
OCAMLC usercontrib/Ltac2/tac2tactics.mli
OCAMLC usercontrib/Ltac2/tac2tactics.ml
OCAMLC usercontrib/Ltac2/tac2stdlib.mli
OCAMLC usercontrib/Ltac2/tac2stdlib.ml
OCAMLC usercontrib/Ltac2/g_ltac2.ml
OCAMLC pack o usercontrib/Ltac2/ltac2_plugin.cmo
OCAMLC plugins/micromega/zify.mli
OCAMLC plugins/micromega/zify.ml
OCAMLC plugins/micromega/g_zify.ml
OCAMLC pack o plugins/micromega/zify_plugin.cmo
OCAMLC dev/top_printers.mli
OCAMLC dev/top_printers.ml
OCAMLC dev/vm_printers.ml
OCAMLC checker/votour.mli
OCAMLC checker/votour.ml
OCAMLC o bin/votour.byte
rm f bin/coqc && cp bin/coqc.byte bin/coqc
COQC noinit theories/Init/Notations.v
COQC noinit theories/Init/Ltac.v
COQC noinit theories/Init/Logic.v
COQC noinit theories/Init/Datatypes.v
COQC noinit theories/Init/Logic_Type.v
COQC noinit theories/Init/Specif.v
COQC noinit theories/Init/Decimal.v
COQC noinit theories/Init/Hexadecimal.v
COQC noinit theories/Init/Numeral.v
COQC noinit theories/Init/Nat.v
COQC noinit theories/Init/Byte.v
COQC noinit theories/Init/Peano.v
COQC noinit theories/Init/Wf.v
COQC noinit theories/Init/Tactics.v
COQC noinit theories/Init/Tauto.v
COQC noinit theories/Init/Prelude.v
COQC theories/Bool/Bool.v
COQC theories/Program/Basics.v
COQC theories/Classes/Init.v
COQC theories/Program/Tactics.v
COQC theories/Relations/Relation_Definitions.v
COQC theories/Classes/RelationClasses.v
COQC theories/Classes/Morphisms.v
COQC theories/Classes/CRelationClasses.v
COQC theories/Classes/CMorphisms.v
COQC theories/Classes/Morphisms_Prop.v
COQC theories/Classes/Equivalence.v
COQC theories/Classes/SetoidTactics.v
COQC theories/ssr/ssrclasses.v
COQC theories/ssr/ssrunder.v
COQC theories/ssr/ssrsetoid.v
COQC theories/Setoids/Setoid.v
COQC theories/Structures/Equalities.v
COQC theories/Relations/Relation_Operators.v
COQC theories/Relations/Operators_Properties.v
COQC theories/Relations/Relations.v
COQC theories/Structures/Orders.v
COQC theories/Numbers/NumPrelude.v
COQC theories/Structures/OrdersTac.v
COQC theories/Structures/OrdersFacts.v
COQC theories/Structures/GenericMinMax.v
COQC theories/Numbers/NatInt/NZAxioms.v
COQC theories/Numbers/NatInt/NZBase.v
COQC theories/Numbers/NatInt/NZAdd.v
COQC theories/Numbers/NatInt/NZMul.v
COQC theories/Logic/Decidable.v
COQC theories/Numbers/NatInt/NZOrder.v
COQC theories/Numbers/NatInt/NZAddOrder.v
COQC theories/Numbers/NatInt/NZMulOrder.v
COQC theories/Numbers/NatInt/NZParity.v
COQC theories/Numbers/NatInt/NZPow.v
COQC theories/Numbers/NatInt/NZSqrt.v
COQC theories/Numbers/NatInt/NZLog.v
COQC theories/Numbers/NatInt/NZDiv.v
COQC theories/Numbers/NatInt/NZGcd.v
COQC theories/Numbers/NatInt/NZBits.v
COQC theories/Numbers/Natural/Abstract/NAxioms.v
COQC theories/Numbers/NatInt/NZProperties.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/NMaxMin.v
COQC theories/Numbers/Natural/Abstract/NParity.v
COQC theories/Numbers/Natural/Abstract/NPow.v
COQC theories/Numbers/Natural/Abstract/NSqrt.v
COQC theories/Numbers/Natural/Abstract/NLog.v
COQC theories/Numbers/Natural/Abstract/NDiv.v
COQC theories/Numbers/Natural/Abstract/NGcd.v
COQC theories/Numbers/Natural/Abstract/NLcm.v
COQC theories/Numbers/Natural/Abstract/NBits.v
COQC theories/Numbers/Natural/Abstract/NProperties.v
COQC theories/Arith/PeanoNat.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/Arith/Between.v
COQC theories/Logic/EqdepFacts.v
COQC theories/Logic/Eqdep_dec.v
COQC theories/Arith/Peano_dec.v
COQC theories/Arith/Compare_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/Numbers/BinNums.v
COQC theories/PArith/BinPosDef.v
COQC theories/PArith/BinPos.v
COQC theories/NArith/BinNatDef.v
COQC theories/NArith/BinNat.v
COQC theories/PArith/Pnat.v
COQC theories/NArith/Nnat.v
COQC theories/setoid_ring/Ring_theory.v
COQC theories/Lists/List.v
COQC theories/setoid_ring/BinList.v
COQC theories/Numbers/Integer/Abstract/ZAxioms.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/ZMaxMin.v
COQC theories/Numbers/Integer/Abstract/ZSgnAbs.v
COQC theories/Numbers/Integer/Abstract/ZParity.v
COQC theories/Numbers/Integer/Abstract/ZPow.v
COQC theories/Numbers/Integer/Abstract/ZDivTrunc.v
COQC theories/Numbers/Integer/Abstract/ZDivFloor.v
COQC theories/Numbers/Integer/Abstract/ZGcd.v
COQC theories/Numbers/Integer/Abstract/ZLcm.v
COQC theories/Numbers/Integer/Abstract/ZBits.v
COQC theories/Numbers/Integer/Abstract/ZProperties.v
COQC theories/ZArith/BinIntDef.v
COQC theories/ZArith/BinInt.v
COQC theories/setoid_ring/Ring_polynom.v
COQC theories/Lists/ListTactics.v
COQC theories/ZArith/Zeven.v
COQC theories/ZArith/Zcompare.v
COQC theories/ZArith/Zorder.v
COQC theories/Bool/Sumbool.v
COQC theories/ZArith/ZArith_dec.v
COQC theories/ZArith/Zbool.v
COQC theories/setoid_ring/InitialRing.v
COQC theories/setoid_ring/Ring_tac.v
COQC theories/setoid_ring/Ring_base.v
COQC theories/setoid_ring/Ring.v
COQC theories/setoid_ring/ArithRing.v
COQC theories/Arith/Arith.v
COQC theories/Arith/Bool_nat.v
COQC theories/Arith/Min.v
COQC theories/Arith/Max.v
COQC theories/Arith/Compare.v
COQC theories/Arith/Even.v
COQC theories/Arith/Div2.v
COQC theories/Arith/Euclid.v
COQC theories/Bool/BoolEq.v
COQC theories/Bool/BoolOrder.v
COQC theories/Vectors/Fin.v
COQC theories/Vectors/VectorDef.v
COQC theories/Vectors/VectorSpec.v
COQC theories/Vectors/VectorEq.v
COQC theories/Vectors/Vector.v
COQC theories/Bool/Bvector.v
COQC theories/Bool/DecBool.v
COQC theories/Bool/IfProp.v
COQC theories/Bool/Zerob.v
COQC theories/Classes/CEquivalence.v
COQC theories/ZArith/Zminmax.v
COQC theories/ZArith/Zmin.v
COQC theories/ZArith/Zmax.v
COQC theories/ZArith/Znat.v
COQC theories/ZArith/Zabs.v
COQC theories/ZArith/auxiliary.v
COQC theories/ZArith/Zmisc.v
COQC theories/ZArith/Wf_Z.v
COQC theories/ZArith/Zhints.v
COQC theories/ZArith/ZArith_base.v
COQC theories/ZArith/Zpow_def.v
COQC theories/omega/OmegaLemmas.v
COQC theories/micromega/ZifyClasses.v
COQC theories/micromega/ZifyInst.v
COQC theories/micromega/Zify.v
COQC theories/omega/PreOmega.v
COQC theories/micromega/OrderedRing.v
COQC theories/NArith/Ndiv_def.v
COQC theories/NArith/Nsqrt_def.v
COQC theories/NArith/Ngcd_def.v
COQC theories/Strings/Byte.v
COQC theories/Strings/Ascii.v
COQC theories/Strings/String.v
COQC theories/Strings/ByteVector.v
COQC theories/NArith/Ndigits.v
COQC theories/setoid_ring/NArithRing.v
COQC theories/NArith/NArith.v
COQC theories/micromega/Env.v
COQC theories/micromega/EnvRing.v
COQC theories/micromega/Refl.v
COQC theories/micromega/Tauto.v
COQC theories/micromega/RingMicromega.v
COQC theories/setoid_ring/ZArithRing.v
COQC theories/micromega/ZCoeff.v
COQC theories/micromega/Ztac.v
COQC theories/ZArith/Zcomplements.v
COQC theories/ZArith/Zdiv.v
COQC theories/ZArith/Znumtheory.v
COQC theories/QArith/QArith_base.v
COQC theories/setoid_ring/Field_theory.v
COQC theories/setoid_ring/Field_tac.v
COQC theories/setoid_ring/Field.v
COQC theories/QArith/Qfield.v
COQC theories/QArith/Qring.v
COQC theories/QArith/Qreduction.v
COQC theories/QArith/QArith.v
COQC theories/micromega/VarMap.v
COQC theories/micromega/ZMicromega.v
COQC theories/micromega/DeclConstant.v
COQC theories/micromega/Lia.v
COQC theories/micromega/ZArith_hints.v
COQC theories/omega/Omega.v
COQC theories/ZArith/Zpower.v
COQC theories/ZArith/ZArith.v
COQC theories/Classes/DecidableClass.v
COQC theories/Program/Utils.v
COQC theories/Logic/ProofIrrelevanceFacts.v
COQC theories/Logic/ProofIrrelevance.v
COQC theories/Logic/FunctionalExtensionality.v
COQC theories/extraction/Extraction.v
COQC theories/Program/Wf.v
COQC theories/Logic/Eqdep.v
COQC theories/Logic/JMeq.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/Sets/Relations_1.v
COQC theories/Sorting/Sorted.v
COQC theories/Lists/SetoidList.v
COQC theories/Classes/RelationPairs.v
COQC theories/Classes/SetoidClass.v
COQC theories/Classes/SetoidDec.v
COQC theories/Compat/AdmitAxiom.v
COQC theories/Compat/Coq812.v
COQC theories/Compat/Coq811.v
COQC theories/Compat/Coq810.v
COQC theories/funind/FunInd.v
COQC theories/Structures/DecidableType.v
COQC theories/Structures/OrderedType.v
COQC theories/FSets/FMapInterface.v
COQC theories/FSets/FMapList.v
COQC theories/ZArith/Int.v
COQC theories/FSets/FMapAVL.v
COQC theories/NArith/Ndec.v
COQC theories/Structures/OrderedTypeEx.v
COQC theories/Structures/DecidableTypeEx.v
COQC theories/FSets/FMapFacts.v
COQC theories/funind/Recdef.v
COQC theories/FSets/FMapFullAVL.v
COQC theories/FSets/FMapPositive.v
COQC theories/FSets/FMapWeakList.v
COQC theories/Structures/OrderedTypeAlt.v
COQC theories/FSets/FMaps.v
COQC theories/FSets/FSetInterface.v
COQC theories/FSets/FSetFacts.v
COQC theories/MSets/MSetInterface.v
COQC theories/MSets/MSetFacts.v
COQC theories/FSets/FSetCompat.v
COQC theories/MSets/MSetGenTree.v
COQC theories/MSets/MSetAVL.v
COQC theories/Structures/OrdersAlt.v
COQC theories/FSets/FSetAVL.v
COQC theories/FSets/FSetBridge.v
COQC theories/FSets/FSetDecide.v
COQC theories/FSets/FSetProperties.v
COQC theories/FSets/FSetEqProperties.v
COQC theories/Structures/EqualitiesFacts.v
COQC theories/Structures/OrdersLists.v
COQC theories/MSets/MSetList.v
COQC theories/FSets/FSetList.v
COQC theories/FSets/FSetPositive.v
COQC theories/Sets/Ensembles.v
COQC theories/Sets/Constructive_sets.v
COQC theories/Sets/Finite_sets.v
COQC theories/FSets/FSetToFiniteSet.v
COQC theories/MSets/MSetWeakList.v
COQC theories/FSets/FSetWeakList.v
COQC theories/FSets/FSets.v
COQC theories/Unicode/Utf8_core.v
COQC theories/Unicode/Utf8.v
COQC theories/Numbers/Cyclic/Abstract/DoubleType.v
COQC theories/ZArith/Zpow_facts.v
COQC theories/ZArith/Zgcd_alt.v
COQC theories/Numbers/Cyclic/Int63/Int63.v
COQC theories/Floats/FloatClass.v
COQC theories/Floats/SpecFloat.v
COQC theories/Floats/PrimFloat.v
COQC theories/Floats/FloatOps.v
COQC theories/Floats/FloatAxioms.v
COQC theories/micromega/QMicromega.v
COQC theories/Logic/HLevels.v
COQC theories/QArith/Qabs.v
COQC theories/QArith/Qround.v
COQC theories/Logic/ConstructiveEpsilon.v
COQC theories/Reals/Cauchy/ConstructiveCauchyReals.v
COQC theories/Reals/Abstract/ConstructiveReals.v
COQC theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v
COQC theories/Reals/Cauchy/ConstructiveCauchyAbs.v
COQC theories/Reals/Cauchy/ConstructiveRcomplete.v
COQC theories/Reals/ClassicalDedekindReals.v
COQC theories/Reals/Abstract/ConstructiveAbs.v
COQC theories/Reals/Abstract/ConstructiveLimits.v
COQC theories/Reals/Abstract/ConstructiveLUB.v
COQC theories/Reals/Rdefinitions.v
COQC theories/Reals/Raxioms.v
COQC theories/Reals/Rpow_def.v
COQC theories/setoid_ring/RealField.v
COQC theories/Reals/RIneq.v
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/QArith/Qreals.v
COQC theories/micromega/RMicromega.v
COQC theories/Reals/Rregisternames.v
COQC theories/micromega/Lra.v
COQC theories/micromega/Lqa.v
COQC theories/micromega/Psatz.v
COQC theories/Floats/FloatLemmas.v
COQC theories/Floats/Floats.v
COQC theories/Lists/ListDec.v
COQC theories/Lists/ListSet.v
COQC theories/Logic/FinFun.v
COQC theories/Sorting/Permutation.v
COQC theories/Lists/SetoidPermutation.v
COQC theories/Lists/Streams.v
COQC theories/Lists/StreamMemo.v
COQC theories/Logic/Berardi.v
COQC theories/Logic/PropExtensionalityFacts.v
COQC theories/Logic/Hurkens.v
COQC theories/Logic/ClassicalFacts.v
COQC theories/Logic/ChoiceFacts.v
COQC theories/Logic/Classical_Prop.v
COQC theories/Logic/Classical_Pred_Type.v
COQC theories/Logic/Classical.v
COQC theories/Logic/ClassicalUniqueChoice.v
COQC theories/Logic/RelationalChoice.v
COQC theories/Logic/ClassicalChoice.v
COQC theories/Logic/Description.v
COQC theories/Logic/ClassicalDescription.v
COQC theories/Logic/ClassicalEpsilon.v
COQC theories/Logic/Diaconescu.v
COQC theories/Logic/Epsilon.v
COQC theories/Logic/ExtensionalityFacts.v
COQC theories/Logic/ExtensionalFunctionRepresentative.v
COQC theories/Logic/IndefiniteDescription.v
COQC theories/Logic/PropExtensionality.v
COQC theories/Logic/PropFacts.v
COQC theories/Logic/SetIsType.v
COQC theories/Logic/SetoidChoice.v
COQC theories/Logic/StrictProp.v
COQC theories/Logic/WeakFan.v
COQC theories/Logic/WKL.v
COQC theories/MSets/MSetDecide.v
COQC theories/MSets/MSetProperties.v
COQC theories/MSets/MSetEqProperties.v
COQC theories/PArith/POrderedType.v
COQC theories/Structures/OrdersEx.v
COQC theories/MSets/MSetPositive.v
COQC theories/MSets/MSetRBT.v
COQC theories/MSets/MSetToFiniteSet.v
COQC theories/MSets/MSets.v
COQC theories/NArith/Ndist.v
COQC theories/Numbers/AltBinNotations.v
COQC theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
COQC theories/Numbers/Cyclic/Abstract/NZCyclic.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/Int63/Cyclic63.v
COQC theories/Numbers/Cyclic/Int63/Ring63.v
COQC theories/Numbers/Cyclic/ZModulo/ZModulo.v
COQC theories/Numbers/DecimalFacts.v
COQC theories/PArith/PArith.v
COQC theories/Numbers/DecimalPos.v
COQC theories/Numbers/DecimalN.v
COQC theories/Numbers/DecimalNat.v
COQC theories/Numbers/DecimalZ.v
COQC theories/Numbers/DecimalQ.v
COQC theories/Numbers/DecimalString.v
COQC theories/Numbers/HexadecimalFacts.v
COQC theories/Numbers/HexadecimalPos.v
COQC theories/Numbers/HexadecimalN.v
COQC theories/Numbers/HexadecimalNat.v
COQC theories/Numbers/HexadecimalZ.v
COQC theories/Numbers/HexadecimalQ.v
COQC theories/Numbers/HexadecimalString.v
COQC theories/Numbers/Integer/Abstract/ZDivEucl.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
COQC theories/QArith/QOrderedType.v
COQC theories/QArith/Qcanon.v
COQC theories/QArith/Qcabs.v
COQC theories/QArith/Qminmax.v
COQC theories/QArith/Qpower.v
COQC theories/Reals/Abstract/ConstructiveRealsMorphisms.v
COQC theories/Reals/Abstract/ConstructiveMinMax.v
COQC theories/Reals/Abstract/ConstructiveSum.v
COQC theories/Reals/Abstract/ConstructivePower.v
COQC theories/Reals/DiscrR.v
COQC theories/Reals/Rbase.v
COQC theories/Reals/Rseries.v
COQC theories/Reals/SeqProp.v
COQC theories/Reals/Rcomplete.v
COQC theories/Reals/PartSum.v
COQC theories/Reals/Alembert.v
COQC theories/Reals/AltSeries.v
COQC theories/Reals/Binomial.v
COQC theories/Reals/Cauchy_prod.v
COQC theories/Reals/ClassicalConstructiveReals.v
COQC theories/Reals/Rsigma.v
COQC theories/Reals/Rprod.v
COQC theories/Reals/SeqSeries.v
COQC theories/Reals/Rtrigo_fun.v
COQC theories/Reals/Rtrigo_def.v
COQC theories/Reals/Cos_rel.v
COQC theories/Reals/Cos_plus.v
COQC theories/Reals/Rtrigo_alt.v
COQC theories/Reals/Rlimit.v
COQC theories/Reals/Rderiv.v
COQC theories/Reals/Ranalysis1.v
COQC theories/Reals/Rsqrt_def.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/Rtrigo1.v
COQC theories/Reals/Exp_prop.v
COQC theories/Reals/Ranalysis2.v
COQC theories/Reals/Ranalysis3.v
COQC theories/Reals/Rtrigo_reg.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_reg.v
COQC theories/Reals/Rtrigo_facts.v
COQC theories/Reals/RiemannInt_SF.v
COQC theories/Reals/RiemannInt.v
COQC theories/Reals/Ranalysis5.v
COQC theories/Reals/Ratan.v
COQC theories/Reals/Machin.v
COQC theories/Reals/Rtrigo.v
COQC theories/Reals/Ranalysis.v
COQC theories/Reals/NewtonInt.v
COQC theories/Reals/Integration.v
COQC theories/Reals/ROrderedType.v
COQC theories/micromega/Fourier_util.v
COQC theories/micromega/Fourier.v
COQC theories/Reals/Reals.v
COQC theories/Reals/Rlogic.v
COQC theories/Reals/Rminmax.v
COQC theories/Reals/Runcountable.v
COQC theories/Sets/Classical_sets.v
COQC theories/Sets/Partial_Order.v
COQC theories/Sets/Cpo.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/Sorting/CPermutation.v
COQC theories/Sorting/PermutSetoid.v
COQC theories/Sorting/Mergesort.v
COQC theories/Sorting/Sorting.v
COQC theories/Sorting/Heap.v
COQC theories/Sorting/PermutEq.v
COQC theories/Strings/BinaryString.v
COQC theories/Strings/HexString.v
COQC theories/Strings/OctalString.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/ZArith/Zdigits.v
COQC theories/ZArith/Zeuclid.v
COQC theories/ZArith/Zpow_alt.v
COQC theories/ZArith/Zquot.v
COQC theories/ZArith/Zwf.v
COQC theories/btauto/Algebra.v
COQC theories/btauto/Reflect.v
COQC theories/btauto/Btauto.v
COQC theories/derive/Derive.v
COQC theories/ssrmatching/ssrmatching.v
COQC theories/ssr/ssreflect.v
COQC theories/ssr/ssrfun.v
COQC theories/ssr/ssrbool.v
COQC theories/extraction/ExtrHaskellBasic.v
COQC theories/extraction/ExtrHaskellNatNum.v
COQC theories/extraction/ExtrHaskellNatInt.v
COQC theories/extraction/ExtrHaskellNatInteger.v
COQC theories/extraction/ExtrHaskellString.v
COQC theories/extraction/ExtrHaskellZNum.v
COQC theories/extraction/ExtrHaskellZInt.v
COQC theories/extraction/ExtrHaskellZInteger.v
COQC theories/extraction/ExtrOCamlFloats.v
COQC theories/extraction/ExtrOCamlInt63.v
COQC theories/extraction/ExtrOcamlBasic.v
COQC theories/extraction/ExtrOcamlBigIntConv.v
COQC theories/extraction/ExtrOcamlChar.v
COQC theories/extraction/ExtrOcamlIntConv.v
COQC theories/extraction/ExtrOcamlNatBigInt.v
COQC theories/extraction/ExtrOcamlNatInt.v
COQC theories/extraction/ExtrOcamlString.v
COQC theories/extraction/ExtrOcamlNativeString.v
COQC theories/extraction/ExtrOcamlZBigInt.v
COQC theories/extraction/ExtrOcamlZInt.v
COQC theories/micromega/MExtraction.v
COQC theories/micromega/ZifyBool.v
COQC theories/micromega/ZifyComparison.v
COQC theories/micromega/ZifyPow.v
COQC theories/setoid_ring/Algebra_syntax.v
COQC theories/setoid_ring/Ncring.v
COQC theories/setoid_ring/Ncring_polynom.v
COQC theories/setoid_ring/Ncring_initial.v
COQC theories/setoid_ring/Ncring_tac.v
COQC theories/setoid_ring/Cring.v
COQC theories/setoid_ring/Integral_domain.v
COQC theories/nsatz/NsatzTactic.v
COQC theories/nsatz/Nsatz.v
COQC theories/omega/OmegaPlugin.v
COQC theories/omega/OmegaTactic.v
COQC theories/rtauto/Bintree.v
COQC theories/rtauto/Rtauto.v
COQC theories/setoid_ring/Rings_Q.v
COQC theories/setoid_ring/Rings_R.v
COQC theories/setoid_ring/Rings_Z.v
COQC theories/ssrsearch/ssrsearch.v
COQC usercontrib/Ltac2/Init.v
COQC usercontrib/Ltac2/Int.v
COQC usercontrib/Ltac2/Message.v
COQC usercontrib/Ltac2/Control.v
COQC usercontrib/Ltac2/Bool.v
COQC usercontrib/Ltac2/Array.v
COQC usercontrib/Ltac2/Char.v
COQC usercontrib/Ltac2/Constr.v
COQC usercontrib/Ltac2/Std.v
COQC usercontrib/Ltac2/Env.v
COQC usercontrib/Ltac2/List.v
COQC usercontrib/Ltac2/Fresh.v
COQC usercontrib/Ltac2/Ident.v
COQC usercontrib/Ltac2/Ltac1.v
COQC usercontrib/Ltac2/String.v
COQC usercontrib/Ltac2/Pattern.v
COQC usercontrib/Ltac2/Notations.v
COQC usercontrib/Ltac2/Ltac2.v
COQC usercontrib/Ltac2/Option.v
rm f bin/coqtop && cp bin/coqtop.byte bin/coqtop
rm f bin/coqchk && cp bin/coqchk.byte bin/coqchk
OCAMLC plugins/micromega/sos_lib.mli
OCAMLC plugins/micromega/sos_lib.ml
OCAMLC plugins/micromega/sos.mli
OCAMLC plugins/micromega/sos.ml
OCAMLC plugins/micromega/csdpcert.mli
OCAMLC plugins/micromega/csdpcert.ml
OCAMLBEST o plugins/micromega/csdpcert
OCAMLC ide/fake_ide.ml
rm f bin/coqidetop && cp bin/coqidetop.byte bin/coqidetop
OCAMLBEST o bin/fake_ide
OCAMLC tools/coqdep.ml
OCAMLBEST o bin/coqdep
OCAMLC tools/coq_makefile.ml
OCAMLBEST o bin/coq_makefile
OCAMLC tools/coq_tex.ml
OCAMLBEST o bin/coqtex
OCAMLC tools/coqwc.ml
OCAMLBEST o bin/coqwc
OCAMLC tools/coqdoc/cdglobals.mli
OCAMLC tools/coqdoc/cdglobals.ml
OCAMLC tools/coqdoc/alpha.mli
OCAMLC tools/coqdoc/alpha.ml
OCAMLC tools/coqdoc/index.mli
OCAMLC tools/coqdoc/index.ml
OCAMLC tools/coqdoc/tokens.mli
OCAMLC tools/coqdoc/tokens.ml
OCAMLC tools/coqdoc/output.mli
OCAMLC tools/coqdoc/output.ml
OCAMLC tools/coqdoc/cpretty.mli
OCAMLC tools/coqdoc/cpretty.ml
OCAMLC tools/coqdoc/main.ml
OCAMLBEST o bin/coqdoc
OCAMLC tools/coqworkmgr.ml
OCAMLBEST o bin/coqworkmgr
OCAMLBEST o bin/votour
OCAMLC a bin/doc_grammar
gmake[1]: Nothing to be done for 'documentation'.
rm f bin/coqide && cp bin/coqide.byte bin/coqide
"/usr/local/bin/ocamlfind" ocamlc thread rectypes w +a492741424445485867 safestring strictsequence ide/default_bindings_src.ml o ide/default_bindings_src.exe
ide/default_bindings_src.exe ide/default.bindings
gmake[1]: 'theories/Init/Prelude.vo' is up to date.
gmake[1]: Leaving directory '/usr/obj/ports/coq8.12.0/coq8.12.0'
gmake: 'coq' is up to date.
gmake: 'documentation' is up to date.
gmake: 'bin/coqide' is up to date.
gmake: 'coqidefiles' is up to date.
gmake: 'theories/Init/Prelude.vo' is up to date.
>>> Running fake in math/coq at 1600015230.06
===> math/coq
===> Faking installation for coq8.12.0
rm f
gmake warnundefinedvariable nobuiltinrules f Makefile.build installcoq installbyte installmeta
gmake[1]: Entering directory '/usr/obj/ports/coq8.12.0/coq8.12.0'
Makefile.install:82: warning: undefined variable 'OLDROOT'
Makefile.install:84: warning: undefined variable 'OLDROOT'
Makefile.install:85: warning: undefined variable 'OLDROOT'
Makefile.install:86: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
# copy style files for coqide
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/tools/coqdoc
install m 644 tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/tools/coqdoc
install bin/coqdep bin/coq_makefile bin/coqtex bin/coqwc bin/coqdoc bin/coqc bin/coqworkmgr bin/coqpp bin/votour bin/ocamllibdep "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
Makefile.install:70: warning: undefined variable 'OLDROOT'
Makefile.install:71: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
install bin/coqc bin/coqchk bin/coqtop bin/coqtop.byte bin/coqproofworker.byte bin/coqtacticworker.byte bin/coqqueryworker.byte "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
Makefile.install:122: warning: undefined variable 'OLDROOT'
Makefile.install:123: warning: undefined variable 'OLDROOT'
Makefile.install:124: warning: undefined variable 'OLDROOT'
Makefile.install:125: warning: undefined variable 'OLDROOT'
Makefile.install:126: warning: undefined variable 'OLDROOT'
Makefile.install:127: warning: undefined variable 'OLDROOT'
Makefile.install:128: warning: undefined variable 'OLDROOT'
Makefile.install:129: warning: undefined variable 'OLDROOT'
Makefile.install:130: warning: undefined variable 'OLDROOT'
Makefile.install:131: warning: undefined variable 'OLDROOT'
Makefile.install:132: warning: undefined variable 'OLDROOT'
Makefile.install:133: warning: undefined variable 'OLDROOT'
Makefile.install:134: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" theories/Arith/Arith.vo theories/Arith/Arith_base.vo theories/Arith/Between.vo theories/Arith/Bool_nat.vo theories/Arith/Compare.vo theories/Arith/Compare_dec.vo theories/Arith/Div2.vo theories/Arith/EqNat.vo theories/Arith/Euclid.vo theories/Arith/Even.vo theories/Arith/Factorial.vo theories/Arith/Gt.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Max.vo theories/Arith/Min.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/PeanoNat.vo theories/Arith/Peano_dec.vo theories/Arith/Plus.vo theories/Arith/Wf_nat.vo theories/Bool/Bool.vo theories/Bool/BoolEq.vo theories/Bool/BoolOrder.vo theories/Bool/Bvector.vo theories/Bool/DecBool.vo theories/Bool/IfProp.vo theories/Bool/Sumbool.vo theories/Bool/Zerob.vo theories/Classes/CEquivalence.vo theories/Classes/CMorphisms.vo theories/Classes/CRelationClasses.vo theories/Classes/DecidableClass.vo theories/Classes/EquivDec.vo theories/Classes/Equivalence.vo theories/Classes/Init.vo theories/Classes/Morphisms.vo theories/Classes/Morphisms_Prop.vo theories/Classes/Morphisms_Relations.vo theories/Classes/RelationClasses.vo theories/Classes/RelationPairs.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidDec.vo theories/Classes/SetoidTactics.vo theories/Compat/AdmitAxiom.vo theories/Compat/Coq810.vo theories/Compat/Coq811.vo theories/Compat/Coq812.vo theories/FSets/FMapAVL.vo theories/FSets/FMapFacts.vo theories/FSets/FMapFullAVL.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/FSets/FMapPositive.vo theories/FSets/FMapWeakList.vo theories/FSets/FMaps.vo theories/FSets/FSetAVL.vo theories/FSets/FSetBridge.vo theories/FSets/FSetCompat.vo theories/FSets/FSetDecide.vo theories/FSets/FSetEqProperties.vo theories/FSets/FSetFacts.vo theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo theories/FSets/FSetPositive.vo theories/FSets/FSetProperties.vo theories/FSets/FSetToFiniteSet.vo theories/FSets/FSetWeakList.vo theories/FSets/FSets.vo theories/Floats/FloatAxioms.vo theories/Floats/FloatClass.vo theories/Floats/FloatLemmas.vo theories/Floats/FloatOps.vo theories/Floats/Floats.vo theories/Floats/PrimFloat.vo theories/Floats/SpecFloat.vo theories/Init/Byte.vo theories/Init/Datatypes.vo theories/Init/Decimal.vo theories/Init/Hexadecimal.vo theories/Init/Logic.vo theories/Init/Logic_Type.vo theories/Init/Ltac.vo theories/Init/Nat.vo theories/Init/Notations.vo theories/Init/Numeral.vo theories/Init/Peano.vo theories/Init/Prelude.vo theories/Init/Specif.vo theories/Init/Tactics.vo theories/Init/Tauto.vo theories/Init/Wf.vo theories/Lists/List.vo theories/Lists/ListDec.vo theories/Lists/ListSet.vo theories/Lists/ListTactics.vo theories/Lists/SetoidList.vo theories/Lists/SetoidPermutation.vo theories/Lists/StreamMemo.vo theories/Lists/Streams.vo theories/Logic/Berardi.vo theories/Logic/ChoiceFacts.vo theories/Logic/Classical.vo theories/Logic/ClassicalChoice.vo theories/Logic/ClassicalDescription.vo theories/Logic/ClassicalEpsilon.vo theories/Logic/ClassicalFacts.vo theories/Logic/ClassicalUniqueChoice.vo theories/Logic/Classical_Pred_Type.vo theories/Logic/Classical_Prop.vo theories/Logic/ConstructiveEpsilon.vo theories/Logic/Decidable.vo theories/Logic/Description.vo theories/Logic/Diaconescu.vo theories/Logic/Epsilon.vo theories/Logic/Eqdep.vo theories/Logic/EqdepFacts.vo theories/Logic/Eqdep_dec.vo theories/Logic/ExtensionalityFacts.vo theories/Logic/ExtensionalFunctionRepresentative.vo theories/Logic/FinFun.vo theories/Logic/FunctionalExtensionality.vo theories/Logic/HLevels.vo theories/Logic/Hurkens.vo theories/Logic/IndefiniteDescription.vo theories/Logic/JMeq.vo theories/Logic/ProofIrrelevance.vo theories/Logic/ProofIrrelevanceFacts.vo theories/Logic/PropExtensionality.vo theories/Logic/PropExtensionalityFacts.vo theories/Logic/PropFacts.vo theories/Logic/RelationalChoice.vo theories/Logic/SetIsType.vo theories/Logic/SetoidChoice.vo theories/Logic/StrictProp.vo theories/Logic/WKL.vo theories/Logic/WeakFan.vo theories/MSets/MSetAVL.vo theories/MSets/MSetDecide.vo theories/MSets/MSetEqProperties.vo theories/MSets/MSetFacts.vo theories/MSets/MSetGenTree.vo theories/MSets/MSetInterface.vo theories/MSets/MSetList.vo theories/MSets/MSetPositive.vo theories/MSets/MSetProperties.vo theories/MSets/MSetRBT.vo theories/MSets/MSetToFiniteSet.vo theories/MSets/MSetWeakList.vo theories/MSets/MSets.vo theories/NArith/BinNat.vo theories/NArith/BinNatDef.vo theories/NArith/NArith.vo theories/NArith/Ndec.vo theories/NArith/Ndigits.vo theories/NArith/Ndist.vo theories/NArith/Ndiv_def.vo theories/NArith/Ngcd_def.vo theories/NArith/Nnat.vo theories/NArith/Nsqrt_def.vo theories/Numbers/AltBinNotations.vo theories/Numbers/BinNums.vo theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo theories/Numbers/Cyclic/Abstract/DoubleType.vo theories/Numbers/Cyclic/Abstract/NZCyclic.vo theories/Numbers/Cyclic/Int31/Cyclic31.vo theories/Numbers/Cyclic/Int31/Int31.vo theories/Numbers/Cyclic/Int31/Ring31.vo theories/Numbers/Cyclic/Int63/Cyclic63.vo theories/Numbers/Cyclic/Int63/Int63.vo theories/Numbers/Cyclic/Int63/Ring63.vo theories/Numbers/Cyclic/ZModulo/ZModulo.vo theories/Numbers/DecimalFacts.vo theories/Numbers/DecimalN.vo theories/Numbers/DecimalNat.vo theories/Numbers/DecimalPos.vo theories/Numbers/DecimalQ.vo theories/Numbers/DecimalString.vo theories/Numbers/DecimalZ.vo theories/Numbers/HexadecimalFacts.vo theories/Numbers/HexadecimalN.vo theories/Numbers/HexadecimalNat.vo theories/Numbers/HexadecimalPos.vo theories/Numbers/HexadecimalQ.vo theories/Numbers/HexadecimalString.vo theories/Numbers/HexadecimalZ.vo theories/Numbers/Integer/Abstract/ZAdd.vo theories/Numbers/Integer/Abstract/ZAddOrder.vo theories/Numbers/Integer/Abstract/ZAxioms.vo theories/Numbers/Integer/Abstract/ZBase.vo theories/Numbers/Integer/Abstract/ZBits.vo theories/Numbers/Integer/Abstract/ZDivEucl.vo theories/Numbers/Integer/Abstract/ZDivFloor.vo theories/Numbers/Integer/Abstract/ZDivTrunc.vo theories/Numbers/Integer/Abstract/ZGcd.vo theories/Numbers/Integer/Abstract/ZLcm.vo theories/Numbers/Integer/Abstract/ZLt.vo theories/Numbers/Integer/Abstract/ZMaxMin.vo theories/Numbers/Integer/Abstract/ZMul.vo theories/Numbers/Integer/Abstract/ZMulOrder.vo theories/Numbers/Integer/Abstract/ZParity.vo theories/Numbers/Integer/Abstract/ZPow.vo theories/Numbers/Integer/Abstract/ZProperties.vo theories/Numbers/Integer/Abstract/ZSgnAbs.vo theories/Numbers/Integer/Binary/ZBinary.vo theories/Numbers/Integer/NatPairs/ZNatPairs.vo theories/Numbers/NaryFunctions.vo theories/Numbers/NatInt/NZAdd.vo theories/Numbers/NatInt/NZAddOrder.vo theories/Numbers/NatInt/NZAxioms.vo theories/Numbers/NatInt/NZBase.vo theories/Numbers/NatInt/NZBits.vo theories/Numbers/NatInt/NZDiv.vo theories/Numbers/NatInt/NZDomain.vo theories/Numbers/NatInt/NZGcd.vo theories/Numbers/NatInt/NZLog.vo theories/Numbers/NatInt/NZMul.vo theories/Numbers/NatInt/NZMulOrder.vo theories/Numbers/NatInt/NZOrder.vo theories/Numbers/NatInt/NZParity.vo theories/Numbers/NatInt/NZPow.vo theories/Numbers/NatInt/NZProperties.vo theories/Numbers/NatInt/NZSqrt.vo theories/Numbers/Natural/Abstract/NAdd.vo theories/Numbers/Natural/Abstract/NAddOrder.vo theories/Numbers/Natural/Abstract/NAxioms.vo theories/Numbers/Natural/Abstract/NBase.vo theories/Numbers/Natural/Abstract/NBits.vo theories/Numbers/Natural/Abstract/NDefOps.vo theories/Numbers/Natural/Abstract/NDiv.vo theories/Numbers/Natural/Abstract/NGcd.vo theories/Numbers/Natural/Abstract/NIso.vo theories/Numbers/Natural/Abstract/NLcm.vo theories/Numbers/Natural/Abstract/NLog.vo theories/Numbers/Natural/Abstract/NMaxMin.vo theories/Numbers/Natural/Abstract/NMulOrder.vo theories/Numbers/Natural/Abstract/NOrder.vo theories/Numbers/Natural/Abstract/NParity.vo theories/Numbers/Natural/Abstract/NPow.vo theories/Numbers/Natural/Abstract/NProperties.vo theories/Numbers/Natural/Abstract/NSqrt.vo theories/Numbers/Natural/Abstract/NStrongRec.vo theories/Numbers/Natural/Abstract/NSub.vo theories/Numbers/Natural/Binary/NBinary.vo theories/Numbers/Natural/Peano/NPeano.vo theories/Numbers/NumPrelude.vo theories/PArith/BinPos.vo theories/PArith/BinPosDef.vo theories/PArith/PArith.vo theories/PArith/POrderedType.vo theories/PArith/Pnat.vo theories/Program/Basics.vo theories/Program/Combinators.vo theories/Program/Equality.vo theories/Program/Program.vo theories/Program/Subset.vo theories/Program/Syntax.vo theories/Program/Tactics.vo theories/Program/Utils.vo theories/Program/Wf.vo theories/QArith/QArith.vo theories/QArith/QArith_base.vo theories/QArith/QOrderedType.vo theories/QArith/Qabs.vo theories/QArith/Qcabs.vo theories/QArith/Qcanon.vo theories/QArith/Qfield.vo theories/QArith/Qminmax.vo theories/QArith/Qpower.vo theories/QArith/Qreals.vo theories/QArith/Qreduction.vo theories/QArith/Qring.vo theories/QArith/Qround.vo theories/Reals/Abstract/ConstructiveAbs.vo theories/Reals/Abstract/ConstructiveLUB.vo theories/Reals/Abstract/ConstructiveLimits.vo theories/Reals/Abstract/ConstructiveMinMax.vo theories/Reals/Abstract/ConstructivePower.vo theories/Reals/Abstract/ConstructiveReals.vo theories/Reals/Abstract/ConstructiveRealsMorphisms.vo theories/Reals/Abstract/ConstructiveSum.vo theories/Reals/Alembert.vo theories/Reals/AltSeries.vo theories/Reals/ArithProp.vo theories/Reals/Binomial.vo theories/Reals/Cauchy/ConstructiveCauchyAbs.vo theories/Reals/Cauchy/ConstructiveCauchyReals.vo theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vo theories/Reals/Cauchy/ConstructiveRcomplete.vo theories/Reals/Cauchy_prod.vo theories/Reals/ClassicalConstructiveReals.vo theories/Reals/ClassicalDedekindReals.vo theories/Reals/Cos_plus.vo theories/Reals/Cos_rel.vo theories/Reals/DiscrR.vo theories/Reals/Exp_prop.vo theories/Reals/Integration.vo theories/Reals/MVT.vo theories/Reals/Machin.vo theories/Reals/NewtonInt.vo theories/Reals/PSeries_reg.vo theories/Reals/PartSum.vo theories/Reals/RIneq.vo theories/Reals/RList.vo theories/Reals/ROrderedType.vo theories/Reals/R_Ifp.vo theories/Reals/R_sqr.vo theories/Reals/R_sqrt.vo theories/Reals/Ranalysis.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Ranalysis4.vo theories/Reals/Ranalysis5.vo theories/Reals/Ranalysis_reg.vo theories/Reals/Ratan.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/Rcomplete.vo theories/Reals/Rdefinitions.vo theories/Reals/Rderiv.vo theories/Reals/Reals.vo theories/Reals/Rfunctions.vo theories/Reals/Rgeom.vo theories/Reals/RiemannInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/Rlimit.vo theories/Reals/Rlogic.vo theories/Reals/Rminmax.vo theories/Reals/Rpow_def.vo theories/Reals/Rpower.vo theories/Reals/Rprod.vo theories/Reals/Rregisternames.vo theories/Reals/Rseries.vo theories/Reals/Rsigma.vo theories/Reals/Rsqrt_def.vo theories/Reals/Rtopology.vo theories/Reals/Rtrigo.vo theories/Reals/Rtrigo1.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_facts.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Runcountable.vo theories/Reals/SeqProp.vo theories/Reals/SeqSeries.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/Sqrt_reg.vo theories/Relations/Operators_Properties.vo theories/Relations/Relation_Definitions.vo theories/Relations/Relation_Operators.vo theories/Relations/Relations.vo theories/Setoids/Setoid.vo theories/Sets/Classical_sets.vo theories/Sets/Constructive_sets.vo theories/Sets/Cpo.vo theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/Sets/Finite_sets_facts.vo theories/Sets/Image.vo theories/Sets/Infinite_sets.vo theories/Sets/Integers.vo theories/Sets/Multiset.vo theories/Sets/Partial_Order.vo theories/Sets/Permut.vo theories/Sets/Powerset.vo theories/Sets/Powerset_Classical_facts.vo theories/Sets/Powerset_facts.vo theories/Sets/Relations_1.vo theories/Sets/Relations_1_facts.vo theories/Sets/Relations_2.vo theories/Sets/Relations_2_facts.vo theories/Sets/Relations_3.vo theories/Sets/Relations_3_facts.vo theories/Sets/Uniset.vo theories/Sorting/CPermutation.vo theories/Sorting/Heap.vo theories/Sorting/Mergesort.vo theories/Sorting/PermutEq.vo theories/Sorting/PermutSetoid.vo theories/Sorting/Permutation.vo theories/Sorting/Sorted.vo theories/Sorting/Sorting.vo theories/Strings/Ascii.vo theories/Strings/BinaryString.vo theories/Strings/Byte.vo theories/Strings/ByteVector.vo theories/Strings/HexString.vo theories/Strings/OctalString.vo theories/Strings/String.vo theories/Structures/DecidableType.vo theories/Structures/DecidableTypeEx.vo theories/Structures/Equalities.vo theories/Structures/EqualitiesFacts.vo theories/Structures/GenericMinMax.vo theories/Structures/OrderedType.vo theories/Structures/OrderedTypeAlt.vo theories/Structures/OrderedTypeEx.vo theories/Structures/Orders.vo theories/Structures/OrdersAlt.vo theories/Structures/OrdersEx.vo theories/Structures/OrdersFacts.vo theories/Structures/OrdersLists.vo theories/Structures/OrdersTac.vo theories/Unicode/Utf8.vo theories/Unicode/Utf8_core.vo theories/Vectors/Fin.vo theories/Vectors/Vector.vo theories/Vectors/VectorDef.vo theories/Vectors/VectorEq.vo theories/Vectors/VectorSpec.vo theories/Wellfounded/Disjoint_Union.vo theories/Wellfounded/Inclusion.vo theories/Wellfounded/Inverse_Image.vo theories/Wellfounded/Lexicographic_Exponentiation.vo theories/Wellfounded/Lexicographic_Product.vo theories/Wellfounded/Transitive_Closure.vo theories/Wellfounded/Union.vo theories/Wellfounded/Well_Ordering.vo theories/Wellfounded/Wellfounded.vo theories/ZArith/BinInt.vo theories/ZArith/BinIntDef.vo theories/ZArith/Int.vo theories/ZArith/Wf_Z.vo theories/ZArith/ZArith.vo theories/ZArith/ZArith_base.vo theories/ZArith/ZArith_dec.vo theories/ZArith/Zabs.vo theories/ZArith/Zbool.vo theories/ZArith/Zcompare.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zdigits.vo theories/ZArith/Zdiv.vo theories/ZArith/Zeuclid.vo theories/ZArith/Zeven.vo theories/ZArith/Zgcd_alt.vo theories/ZArith/Zhints.vo theories/ZArith/Zmax.vo theories/ZArith/Zmin.vo theories/ZArith/Zminmax.vo theories/ZArith/Zmisc.vo theories/ZArith/Znat.vo theories/ZArith/Znumtheory.vo theories/ZArith/Zorder.vo theories/ZArith/Zpow_alt.vo theories/ZArith/Zpow_def.vo theories/ZArith/Zpow_facts.vo theories/ZArith/Zpower.vo theories/ZArith/Zquot.vo theories/ZArith/Zwf.vo theories/ZArith/auxiliary.vo theories/btauto/Algebra.vo theories/btauto/Btauto.vo theories/btauto/Reflect.vo theories/derive/Derive.vo theories/ssr/ssrbool.vo theories/ssr/ssrclasses.vo theories/ssr/ssreflect.vo theories/ssr/ssrfun.vo theories/ssr/ssrsetoid.vo theories/ssr/ssrunder.vo theories/extraction/ExtrHaskellBasic.vo theories/extraction/ExtrHaskellNatInt.vo theories/extraction/ExtrHaskellNatInteger.vo theories/extraction/ExtrHaskellNatNum.vo theories/extraction/ExtrHaskellString.vo theories/extraction/ExtrHaskellZInt.vo theories/extraction/ExtrHaskellZInteger.vo theories/extraction/ExtrHaskellZNum.vo theories/extraction/ExtrOCamlFloats.vo theories/extraction/ExtrOCamlInt63.vo theories/extraction/ExtrOcamlBasic.vo theories/extraction/ExtrOcamlBigIntConv.vo theories/extraction/ExtrOcamlChar.vo theories/extraction/ExtrOcamlIntConv.vo theories/extraction/ExtrOcamlNatBigInt.vo theories/extraction/ExtrOcamlNatInt.vo theories/extraction/ExtrOcamlString.vo theories/extraction/ExtrOcamlNativeString.vo theories/extraction/ExtrOcamlZBigInt.vo theories/extraction/ExtrOcamlZInt.vo theories/extraction/Extraction.vo theories/funind/FunInd.vo theories/funind/Recdef.vo theories/micromega/DeclConstant.vo theories/micromega/Env.vo theories/micromega/EnvRing.vo theories/micromega/Fourier.vo theories/micromega/Fourier_util.vo theories/micromega/Lia.vo theories/micromega/Lqa.vo theories/micromega/Lra.vo theories/micromega/MExtraction.vo theories/micromega/OrderedRing.vo theories/micromega/Psatz.vo theories/micromega/QMicromega.vo theories/micromega/RMicromega.vo theories/micromega/Refl.vo theories/micromega/RingMicromega.vo theories/micromega/Tauto.vo theories/micromega/VarMap.vo theories/micromega/ZArith_hints.vo theories/micromega/ZCoeff.vo theories/micromega/ZMicromega.vo theories/micromega/Zify.vo theories/micromega/ZifyBool.vo theories/micromega/ZifyClasses.vo theories/micromega/ZifyInst.vo theories/micromega/ZifyComparison.vo theories/micromega/ZifyPow.vo theories/micromega/Ztac.vo theories/nsatz/Nsatz.vo theories/nsatz/NsatzTactic.vo theories/omega/Omega.vo theories/omega/OmegaLemmas.vo theories/omega/OmegaPlugin.vo theories/omega/OmegaTactic.vo theories/omega/PreOmega.vo theories/rtauto/Bintree.vo theories/rtauto/Rtauto.vo theories/setoid_ring/Algebra_syntax.vo theories/setoid_ring/ArithRing.vo theories/setoid_ring/BinList.vo theories/setoid_ring/Cring.vo theories/setoid_ring/Field.vo theories/setoid_ring/Field_tac.vo theories/setoid_ring/Field_theory.vo theories/setoid_ring/InitialRing.vo theories/setoid_ring/Integral_domain.vo theories/setoid_ring/NArithRing.vo theories/setoid_ring/Ncring.vo theories/setoid_ring/Ncring_initial.vo theories/setoid_ring/Ncring_polynom.vo theories/setoid_ring/Ncring_tac.vo theories/setoid_ring/RealField.vo theories/setoid_ring/Ring.vo theories/setoid_ring/Ring_base.vo theories/setoid_ring/Ring_polynom.vo theories/setoid_ring/Ring_tac.vo theories/setoid_ring/Ring_theory.vo theories/setoid_ring/Rings_Q.vo theories/setoid_ring/Rings_R.vo theories/setoid_ring/Rings_Z.vo theories/setoid_ring/ZArithRing.vo theories/ssrmatching/ssrmatching.vo theories/ssrsearch/ssrsearch.vo usercontrib/Ltac2/Array.vo usercontrib/Ltac2/Bool.vo usercontrib/Ltac2/Char.vo usercontrib/Ltac2/Constr.vo usercontrib/Ltac2/Control.vo usercontrib/Ltac2/Env.vo usercontrib/Ltac2/Fresh.vo usercontrib/Ltac2/Ident.vo usercontrib/Ltac2/Init.vo usercontrib/Ltac2/Int.vo usercontrib/Ltac2/List.vo usercontrib/Ltac2/Ltac1.vo usercontrib/Ltac2/Ltac2.vo usercontrib/Ltac2/Message.vo usercontrib/Ltac2/Notations.vo usercontrib/Ltac2/Option.vo usercontrib/Ltac2/Pattern.vo usercontrib/Ltac2/Std.vo usercontrib/Ltac2/String.vo
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" theories/Arith/Arith.vos theories/Arith/Arith_base.vos theories/Arith/Between.vos theories/Arith/Bool_nat.vos theories/Arith/Compare.vos theories/Arith/Compare_dec.vos theories/Arith/Div2.vos theories/Arith/EqNat.vos theories/Arith/Euclid.vos theories/Arith/Even.vos theories/Arith/Factorial.vos theories/Arith/Gt.vos theories/Arith/Le.vos theories/Arith/Lt.vos theories/Arith/Max.vos theories/Arith/Min.vos theories/Arith/Minus.vos theories/Arith/Mult.vos theories/Arith/PeanoNat.vos theories/Arith/Peano_dec.vos theories/Arith/Plus.vos theories/Arith/Wf_nat.vos theories/Bool/Bool.vos theories/Bool/BoolEq.vos theories/Bool/BoolOrder.vos theories/Bool/Bvector.vos theories/Bool/DecBool.vos theories/Bool/IfProp.vos theories/Bool/Sumbool.vos theories/Bool/Zerob.vos theories/Classes/CEquivalence.vos theories/Classes/CMorphisms.vos theories/Classes/CRelationClasses.vos theories/Classes/DecidableClass.vos theories/Classes/EquivDec.vos theories/Classes/Equivalence.vos theories/Classes/Init.vos theories/Classes/Morphisms.vos theories/Classes/Morphisms_Prop.vos theories/Classes/Morphisms_Relations.vos theories/Classes/RelationClasses.vos theories/Classes/RelationPairs.vos theories/Classes/SetoidClass.vos theories/Classes/SetoidDec.vos theories/Classes/SetoidTactics.vos theories/Compat/AdmitAxiom.vos theories/Compat/Coq810.vos theories/Compat/Coq811.vos theories/Compat/Coq812.vos theories/FSets/FMapAVL.vos theories/FSets/FMapFacts.vos theories/FSets/FMapFullAVL.vos theories/FSets/FMapInterface.vos theories/FSets/FMapList.vos theories/FSets/FMapPositive.vos theories/FSets/FMapWeakList.vos theories/FSets/FMaps.vos theories/FSets/FSetAVL.vos theories/FSets/FSetBridge.vos theories/FSets/FSetCompat.vos theories/FSets/FSetDecide.vos theories/FSets/FSetEqProperties.vos theories/FSets/FSetFacts.vos theories/FSets/FSetInterface.vos theories/FSets/FSetList.vos theories/FSets/FSetPositive.vos theories/FSets/FSetProperties.vos theories/FSets/FSetToFiniteSet.vos theories/FSets/FSetWeakList.vos theories/FSets/FSets.vos theories/Floats/FloatAxioms.vos theories/Floats/FloatClass.vos theories/Floats/FloatLemmas.vos theories/Floats/FloatOps.vos theories/Floats/Floats.vos theories/Floats/PrimFloat.vos theories/Floats/SpecFloat.vos theories/Init/Byte.vos theories/Init/Datatypes.vos theories/Init/Decimal.vos theories/Init/Hexadecimal.vos theories/Init/Logic.vos theories/Init/Logic_Type.vos theories/Init/Ltac.vos theories/Init/Nat.vos theories/Init/Notations.vos theories/Init/Numeral.vos theories/Init/Peano.vos theories/Init/Prelude.vos theories/Init/Specif.vos theories/Init/Tactics.vos theories/Init/Tauto.vos theories/Init/Wf.vos theories/Lists/List.vos theories/Lists/ListDec.vos theories/Lists/ListSet.vos theories/Lists/ListTactics.vos theories/Lists/SetoidList.vos theories/Lists/SetoidPermutation.vos theories/Lists/StreamMemo.vos theories/Lists/Streams.vos theories/Logic/Berardi.vos theories/Logic/ChoiceFacts.vos theories/Logic/Classical.vos theories/Logic/ClassicalChoice.vos theories/Logic/ClassicalDescription.vos theories/Logic/ClassicalEpsilon.vos theories/Logic/ClassicalFacts.vos theories/Logic/ClassicalUniqueChoice.vos theories/Logic/Classical_Pred_Type.vos theories/Logic/Classical_Prop.vos theories/Logic/ConstructiveEpsilon.vos theories/Logic/Decidable.vos theories/Logic/Description.vos theories/Logic/Diaconescu.vos theories/Logic/Epsilon.vos theories/Logic/Eqdep.vos theories/Logic/EqdepFacts.vos theories/Logic/Eqdep_dec.vos theories/Logic/ExtensionalityFacts.vos theories/Logic/ExtensionalFunctionRepresentative.vos theories/Logic/FinFun.vos theories/Logic/FunctionalExtensionality.vos theories/Logic/HLevels.vos theories/Logic/Hurkens.vos theories/Logic/IndefiniteDescription.vos theories/Logic/JMeq.vos theories/Logic/ProofIrrelevance.vos theories/Logic/ProofIrrelevanceFacts.vos theories/Logic/PropExtensionality.vos theories/Logic/PropExtensionalityFacts.vos theories/Logic/PropFacts.vos theories/Logic/RelationalChoice.vos theories/Logic/SetIsType.vos theories/Logic/SetoidChoice.vos theories/Logic/StrictProp.vos theories/Logic/WKL.vos theories/Logic/WeakFan.vos theories/MSets/MSetAVL.vos theories/MSets/MSetDecide.vos theories/MSets/MSetEqProperties.vos theories/MSets/MSetFacts.vos theories/MSets/MSetGenTree.vos theories/MSets/MSetInterface.vos theories/MSets/MSetList.vos theories/MSets/MSetPositive.vos theories/MSets/MSetProperties.vos theories/MSets/MSetRBT.vos theories/MSets/MSetToFiniteSet.vos theories/MSets/MSetWeakList.vos theories/MSets/MSets.vos theories/NArith/BinNat.vos theories/NArith/BinNatDef.vos theories/NArith/NArith.vos theories/NArith/Ndec.vos theories/NArith/Ndigits.vos theories/NArith/Ndist.vos theories/NArith/Ndiv_def.vos theories/NArith/Ngcd_def.vos theories/NArith/Nnat.vos theories/NArith/Nsqrt_def.vos theories/Numbers/AltBinNotations.vos theories/Numbers/BinNums.vos theories/Numbers/Cyclic/Abstract/CyclicAxioms.vos theories/Numbers/Cyclic/Abstract/DoubleType.vos theories/Numbers/Cyclic/Abstract/NZCyclic.vos theories/Numbers/Cyclic/Int31/Cyclic31.vos theories/Numbers/Cyclic/Int31/Int31.vos theories/Numbers/Cyclic/Int31/Ring31.vos theories/Numbers/Cyclic/Int63/Cyclic63.vos theories/Numbers/Cyclic/Int63/Int63.vos theories/Numbers/Cyclic/Int63/Ring63.vos theories/Numbers/Cyclic/ZModulo/ZModulo.vos theories/Numbers/DecimalFacts.vos theories/Numbers/DecimalN.vos theories/Numbers/DecimalNat.vos theories/Numbers/DecimalPos.vos theories/Numbers/DecimalQ.vos theories/Numbers/DecimalString.vos theories/Numbers/DecimalZ.vos theories/Numbers/HexadecimalFacts.vos theories/Numbers/HexadecimalN.vos theories/Numbers/HexadecimalNat.vos theories/Numbers/HexadecimalPos.vos theories/Numbers/HexadecimalQ.vos theories/Numbers/HexadecimalString.vos theories/Numbers/HexadecimalZ.vos theories/Numbers/Integer/Abstract/ZAdd.vos theories/Numbers/Integer/Abstract/ZAddOrder.vos theories/Numbers/Integer/Abstract/ZAxioms.vos theories/Numbers/Integer/Abstract/ZBase.vos theories/Numbers/Integer/Abstract/ZBits.vos theories/Numbers/Integer/Abstract/ZDivEucl.vos theories/Numbers/Integer/Abstract/ZDivFloor.vos theories/Numbers/Integer/Abstract/ZDivTrunc.vos theories/Numbers/Integer/Abstract/ZGcd.vos theories/Numbers/Integer/Abstract/ZLcm.vos theories/Numbers/Integer/Abstract/ZLt.vos theories/Numbers/Integer/Abstract/ZMaxMin.vos theories/Numbers/Integer/Abstract/ZMul.vos theories/Numbers/Integer/Abstract/ZMulOrder.vos theories/Numbers/Integer/Abstract/ZParity.vos theories/Numbers/Integer/Abstract/ZPow.vos theories/Numbers/Integer/Abstract/ZProperties.vos theories/Numbers/Integer/Abstract/ZSgnAbs.vos theories/Numbers/Integer/Binary/ZBinary.vos theories/Numbers/Integer/NatPairs/ZNatPairs.vos theories/Numbers/NaryFunctions.vos theories/Numbers/NatInt/NZAdd.vos theories/Numbers/NatInt/NZAddOrder.vos theories/Numbers/NatInt/NZAxioms.vos theories/Numbers/NatInt/NZBase.vos theories/Numbers/NatInt/NZBits.vos theories/Numbers/NatInt/NZDiv.vos theories/Numbers/NatInt/NZDomain.vos theories/Numbers/NatInt/NZGcd.vos theories/Numbers/NatInt/NZLog.vos theories/Numbers/NatInt/NZMul.vos theories/Numbers/NatInt/NZMulOrder.vos theories/Numbers/NatInt/NZOrder.vos theories/Numbers/NatInt/NZParity.vos theories/Numbers/NatInt/NZPow.vos theories/Numbers/NatInt/NZProperties.vos theories/Numbers/NatInt/NZSqrt.vos theories/Numbers/Natural/Abstract/NAdd.vos theories/Numbers/Natural/Abstract/NAddOrder.vos theories/Numbers/Natural/Abstract/NAxioms.vos theories/Numbers/Natural/Abstract/NBase.vos theories/Numbers/Natural/Abstract/NBits.vos theories/Numbers/Natural/Abstract/NDefOps.vos theories/Numbers/Natural/Abstract/NDiv.vos theories/Numbers/Natural/Abstract/NGcd.vos theories/Numbers/Natural/Abstract/NIso.vos theories/Numbers/Natural/Abstract/NLcm.vos theories/Numbers/Natural/Abstract/NLog.vos theories/Numbers/Natural/Abstract/NMaxMin.vos theories/Numbers/Natural/Abstract/NMulOrder.vos theories/Numbers/Natural/Abstract/NOrder.vos theories/Numbers/Natural/Abstract/NParity.vos theories/Numbers/Natural/Abstract/NPow.vos theories/Numbers/Natural/Abstract/NProperties.vos theories/Numbers/Natural/Abstract/NSqrt.vos theories/Numbers/Natural/Abstract/NStrongRec.vos theories/Numbers/Natural/Abstract/NSub.vos theories/Numbers/Natural/Binary/NBinary.vos theories/Numbers/Natural/Peano/NPeano.vos theories/Numbers/NumPrelude.vos theories/PArith/BinPos.vos theories/PArith/BinPosDef.vos theories/PArith/PArith.vos theories/PArith/POrderedType.vos theories/PArith/Pnat.vos theories/Program/Basics.vos theories/Program/Combinators.vos theories/Program/Equality.vos theories/Program/Program.vos theories/Program/Subset.vos theories/Program/Syntax.vos theories/Program/Tactics.vos theories/Program/Utils.vos theories/Program/Wf.vos theories/QArith/QArith.vos theories/QArith/QArith_base.vos theories/QArith/QOrderedType.vos theories/QArith/Qabs.vos theories/QArith/Qcabs.vos theories/QArith/Qcanon.vos theories/QArith/Qfield.vos theories/QArith/Qminmax.vos theories/QArith/Qpower.vos theories/QArith/Qreals.vos theories/QArith/Qreduction.vos theories/QArith/Qring.vos theories/QArith/Qround.vos theories/Reals/Abstract/ConstructiveAbs.vos theories/Reals/Abstract/ConstructiveLUB.vos theories/Reals/Abstract/ConstructiveLimits.vos theories/Reals/Abstract/ConstructiveMinMax.vos theories/Reals/Abstract/ConstructivePower.vos theories/Reals/Abstract/ConstructiveReals.vos theories/Reals/Abstract/ConstructiveRealsMorphisms.vos theories/Reals/Abstract/ConstructiveSum.vos theories/Reals/Alembert.vos theories/Reals/AltSeries.vos theories/Reals/ArithProp.vos theories/Reals/Binomial.vos theories/Reals/Cauchy/ConstructiveCauchyAbs.vos theories/Reals/Cauchy/ConstructiveCauchyReals.vos theories/Reals/Cauchy/ConstructiveCauchyRealsMult.vos theories/Reals/Cauchy/ConstructiveRcomplete.vos theories/Reals/Cauchy_prod.vos theories/Reals/ClassicalConstructiveReals.vos theories/Reals/ClassicalDedekindReals.vos theories/Reals/Cos_plus.vos theories/Reals/Cos_rel.vos theories/Reals/DiscrR.vos theories/Reals/Exp_prop.vos theories/Reals/Integration.vos theories/Reals/MVT.vos theories/Reals/Machin.vos theories/Reals/NewtonInt.vos theories/Reals/PSeries_reg.vos theories/Reals/PartSum.vos theories/Reals/RIneq.vos theories/Reals/RList.vos theories/Reals/ROrderedType.vos theories/Reals/R_Ifp.vos theories/Reals/R_sqr.vos theories/Reals/R_sqrt.vos theories/Reals/Ranalysis.vos theories/Reals/Ranalysis1.vos theories/Reals/Ranalysis2.vos theories/Reals/Ranalysis3.vos theories/Reals/Ranalysis4.vos theories/Reals/Ranalysis5.vos theories/Reals/Ranalysis_reg.vos theories/Reals/Ratan.vos theories/Reals/Raxioms.vos theories/Reals/Rbase.vos theories/Reals/Rbasic_fun.vos theories/Reals/Rcomplete.vos theories/Reals/Rdefinitions.vos theories/Reals/Rderiv.vos theories/Reals/Reals.vos theories/Reals/Rfunctions.vos theories/Reals/Rgeom.vos theories/Reals/RiemannInt.vos theories/Reals/RiemannInt_SF.vos theories/Reals/Rlimit.vos theories/Reals/Rlogic.vos theories/Reals/Rminmax.vos theories/Reals/Rpow_def.vos theories/Reals/Rpower.vos theories/Reals/Rprod.vos theories/Reals/Rregisternames.vos theories/Reals/Rseries.vos theories/Reals/Rsigma.vos theories/Reals/Rsqrt_def.vos theories/Reals/Rtopology.vos theories/Reals/Rtrigo.vos theories/Reals/Rtrigo1.vos theories/Reals/Rtrigo_alt.vos theories/Reals/Rtrigo_calc.vos theories/Reals/Rtrigo_def.vos theories/Reals/Rtrigo_facts.vos theories/Reals/Rtrigo_fun.vos theories/Reals/Rtrigo_reg.vos theories/Reals/Runcountable.vos theories/Reals/SeqProp.vos theories/Reals/SeqSeries.vos theories/Reals/SplitAbsolu.vos theories/Reals/SplitRmult.vos theories/Reals/Sqrt_reg.vos theories/Relations/Operators_Properties.vos theories/Relations/Relation_Definitions.vos theories/Relations/Relation_Operators.vos theories/Relations/Relations.vos theories/Setoids/Setoid.vos theories/Sets/Classical_sets.vos theories/Sets/Constructive_sets.vos theories/Sets/Cpo.vos theories/Sets/Ensembles.vos theories/Sets/Finite_sets.vos theories/Sets/Finite_sets_facts.vos theories/Sets/Image.vos theories/Sets/Infinite_sets.vos theories/Sets/Integers.vos theories/Sets/Multiset.vos theories/Sets/Partial_Order.vos theories/Sets/Permut.vos theories/Sets/Powerset.vos theories/Sets/Powerset_Classical_facts.vos theories/Sets/Powerset_facts.vos theories/Sets/Relations_1.vos theories/Sets/Relations_1_facts.vos theories/Sets/Relations_2.vos theories/Sets/Relations_2_facts.vos theories/Sets/Relations_3.vos theories/Sets/Relations_3_facts.vos theories/Sets/Uniset.vos theories/Sorting/CPermutation.vos theories/Sorting/Heap.vos theories/Sorting/Mergesort.vos theories/Sorting/PermutEq.vos theories/Sorting/PermutSetoid.vos theories/Sorting/Permutation.vos theories/Sorting/Sorted.vos theories/Sorting/Sorting.vos theories/Strings/Ascii.vos theories/Strings/BinaryString.vos theories/Strings/Byte.vos theories/Strings/ByteVector.vos theories/Strings/HexString.vos theories/Strings/OctalString.vos theories/Strings/String.vos theories/Structures/DecidableType.vos theories/Structures/DecidableTypeEx.vos theories/Structures/Equalities.vos theories/Structures/EqualitiesFacts.vos theories/Structures/GenericMinMax.vos theories/Structures/OrderedType.vos theories/Structures/OrderedTypeAlt.vos theories/Structures/OrderedTypeEx.vos theories/Structures/Orders.vos theories/Structures/OrdersAlt.vos theories/Structures/OrdersEx.vos theories/Structures/OrdersFacts.vos theories/Structures/OrdersLists.vos theories/Structures/OrdersTac.vos theories/Unicode/Utf8.vos theories/Unicode/Utf8_core.vos theories/Vectors/Fin.vos theories/Vectors/Vector.vos theories/Vectors/VectorDef.vos theories/Vectors/VectorEq.vos theories/Vectors/VectorSpec.vos theories/Wellfounded/Disjoint_Union.vos theories/Wellfounded/Inclusion.vos theories/Wellfounded/Inverse_Image.vos theories/Wellfounded/Lexicographic_Exponentiation.vos theories/Wellfounded/Lexicographic_Product.vos theories/Wellfounded/Transitive_Closure.vos theories/Wellfounded/Union.vos theories/Wellfounded/Well_Ordering.vos theories/Wellfounded/Wellfounded.vos theories/ZArith/BinInt.vos theories/ZArith/BinIntDef.vos theories/ZArith/Int.vos theories/ZArith/Wf_Z.vos theories/ZArith/ZArith.vos theories/ZArith/ZArith_base.vos theories/ZArith/ZArith_dec.vos theories/ZArith/Zabs.vos theories/ZArith/Zbool.vos theories/ZArith/Zcompare.vos theories/ZArith/Zcomplements.vos theories/ZArith/Zdigits.vos theories/ZArith/Zdiv.vos theories/ZArith/Zeuclid.vos theories/ZArith/Zeven.vos theories/ZArith/Zgcd_alt.vos theories/ZArith/Zhints.vos theories/ZArith/Zmax.vos theories/ZArith/Zmin.vos theories/ZArith/Zminmax.vos theories/ZArith/Zmisc.vos theories/ZArith/Znat.vos theories/ZArith/Znumtheory.vos theories/ZArith/Zorder.vos theories/ZArith/Zpow_alt.vos theories/ZArith/Zpow_def.vos theories/ZArith/Zpow_facts.vos theories/ZArith/Zpower.vos theories/ZArith/Zquot.vos theories/ZArith/Zwf.vos theories/ZArith/auxiliary.vos theories/btauto/Algebra.vos theories/btauto/Btauto.vos theories/btauto/Reflect.vos theories/derive/Derive.vos theories/ssr/ssrbool.vos theories/ssr/ssrclasses.vos theories/ssr/ssreflect.vos theories/ssr/ssrfun.vos theories/ssr/ssrsetoid.vos theories/ssr/ssrunder.vos theories/extraction/ExtrHaskellBasic.vos theories/extraction/ExtrHaskellNatInt.vos theories/extraction/ExtrHaskellNatInteger.vos theories/extraction/ExtrHaskellNatNum.vos theories/extraction/ExtrHaskellString.vos theories/extraction/ExtrHaskellZInt.vos theories/extraction/ExtrHaskellZInteger.vos theories/extraction/ExtrHaskellZNum.vos theories/extraction/ExtrOCamlFloats.vos theories/extraction/ExtrOCamlInt63.vos theories/extraction/ExtrOcamlBasic.vos theories/extraction/ExtrOcamlBigIntConv.vos theories/extraction/ExtrOcamlChar.vos theories/extraction/ExtrOcamlIntConv.vos theories/extraction/ExtrOcamlNatBigInt.vos theories/extraction/ExtrOcamlNatInt.vos theories/extraction/ExtrOcamlString.vos theories/extraction/ExtrOcamlNativeString.vos theories/extraction/ExtrOcamlZBigInt.vos theories/extraction/ExtrOcamlZInt.vos theories/extraction/Extraction.vos theories/funind/FunInd.vos theories/funind/Recdef.vos theories/micromega/DeclConstant.vos theories/micromega/Env.vos theories/micromega/EnvRing.vos theories/micromega/Fourier.vos theories/micromega/Fourier_util.vos theories/micromega/Lia.vos theories/micromega/Lqa.vos theories/micromega/Lra.vos theories/micromega/MExtraction.vos theories/micromega/OrderedRing.vos theories/micromega/Psatz.vos theories/micromega/QMicromega.vos theories/micromega/RMicromega.vos theories/micromega/Refl.vos theories/micromega/RingMicromega.vos theories/micromega/Tauto.vos theories/micromega/VarMap.vos theories/micromega/ZArith_hints.vos theories/micromega/ZCoeff.vos theories/micromega/ZMicromega.vos theories/micromega/Zify.vos theories/micromega/ZifyBool.vos theories/micromega/ZifyClasses.vos theories/micromega/ZifyInst.vos theories/micromega/ZifyComparison.vos theories/micromega/ZifyPow.vos theories/micromega/Ztac.vos theories/nsatz/Nsatz.vos theories/nsatz/NsatzTactic.vos theories/omega/Omega.vos theories/omega/OmegaLemmas.vos theories/omega/OmegaPlugin.vos theories/omega/OmegaTactic.vos theories/omega/PreOmega.vos theories/rtauto/Bintree.vos theories/rtauto/Rtauto.vos theories/setoid_ring/Algebra_syntax.vos theories/setoid_ring/ArithRing.vos theories/setoid_ring/BinList.vos theories/setoid_ring/Cring.vos theories/setoid_ring/Field.vos theories/setoid_ring/Field_tac.vos theories/setoid_ring/Field_theory.vos theories/setoid_ring/InitialRing.vos theories/setoid_ring/Integral_domain.vos theories/setoid_ring/NArithRing.vos theories/setoid_ring/Ncring.vos theories/setoid_ring/Ncring_initial.vos theories/setoid_ring/Ncring_polynom.vos theories/setoid_ring/Ncring_tac.vos theories/setoid_ring/RealField.vos theories/setoid_ring/Ring.vos theories/setoid_ring/Ring_base.vos theories/setoid_ring/Ring_polynom.vos theories/setoid_ring/Ring_tac.vos theories/setoid_ring/Ring_theory.vos theories/setoid_ring/Rings_Q.vos theories/setoid_ring/Rings_R.vos theories/setoid_ring/Rings_Z.vos theories/setoid_ring/ZArithRing.vos theories/ssrmatching/ssrmatching.vos theories/ssrsearch/ssrsearch.vos usercontrib/Ltac2/Array.vos usercontrib/Ltac2/Bool.vos usercontrib/Ltac2/Char.vos usercontrib/Ltac2/Constr.vos usercontrib/Ltac2/Control.vos usercontrib/Ltac2/Env.vos usercontrib/Ltac2/Fresh.vos usercontrib/Ltac2/Ident.vos usercontrib/Ltac2/Init.vos usercontrib/Ltac2/Int.vos usercontrib/Ltac2/List.vos usercontrib/Ltac2/Ltac1.vos usercontrib/Ltac2/Ltac2.vos usercontrib/Ltac2/Message.vos usercontrib/Ltac2/Notations.vos usercontrib/Ltac2/Option.vos usercontrib/Ltac2/Pattern.vos usercontrib/Ltac2/Std.vos usercontrib/Ltac2/String.vos  true
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" theories/Arith/.coqnative/NCoq_Arith_Arith.cm* theories/Arith/.coqnative/NCoq_Arith_Arith_base.cm* theories/Arith/.coqnative/NCoq_Arith_Between.cm* theories/Arith/.coqnative/NCoq_Arith_Bool_nat.cm* theories/Arith/.coqnative/NCoq_Arith_Compare.cm* theories/Arith/.coqnative/NCoq_Arith_Compare_dec.cm* theories/Arith/.coqnative/NCoq_Arith_Div2.cm* theories/Arith/.coqnative/NCoq_Arith_EqNat.cm* theories/Arith/.coqnative/NCoq_Arith_Euclid.cm* theories/Arith/.coqnative/NCoq_Arith_Even.cm* theories/Arith/.coqnative/NCoq_Arith_Factorial.cm* theories/Arith/.coqnative/NCoq_Arith_Gt.cm* theories/Arith/.coqnative/NCoq_Arith_Le.cm* theories/Arith/.coqnative/NCoq_Arith_Lt.cm* theories/Arith/.coqnative/NCoq_Arith_Max.cm* theories/Arith/.coqnative/NCoq_Arith_Min.cm* theories/Arith/.coqnative/NCoq_Arith_Minus.cm* theories/Arith/.coqnative/NCoq_Arith_Mult.cm* theories/Arith/.coqnative/NCoq_Arith_PeanoNat.cm* theories/Arith/.coqnative/NCoq_Arith_Peano_dec.cm* theories/Arith/.coqnative/NCoq_Arith_Plus.cm* theories/Arith/.coqnative/NCoq_Arith_Wf_nat.cm* theories/Bool/.coqnative/NCoq_Bool_Bool.cm* theories/Bool/.coqnative/NCoq_Bool_BoolEq.cm* theories/Bool/.coqnative/NCoq_Bool_BoolOrder.cm* theories/Bool/.coqnative/NCoq_Bool_Bvector.cm* theories/Bool/.coqnative/NCoq_Bool_DecBool.cm* theories/Bool/.coqnative/NCoq_Bool_IfProp.cm* theories/Bool/.coqnative/NCoq_Bool_Sumbool.cm* theories/Bool/.coqnative/NCoq_Bool_Zerob.cm* theories/Classes/.coqnative/NCoq_Classes_CEquivalence.cm* theories/Classes/.coqnative/NCoq_Classes_CMorphisms.cm* theories/Classes/.coqnative/NCoq_Classes_CRelationClasses.cm* theories/Classes/.coqnative/NCoq_Classes_DecidableClass.cm* theories/Classes/.coqnative/NCoq_Classes_EquivDec.cm* theories/Classes/.coqnative/NCoq_Classes_Equivalence.cm* theories/Classes/.coqnative/NCoq_Classes_Init.cm* theories/Classes/.coqnative/NCoq_Classes_Morphisms.cm* theories/Classes/.coqnative/NCoq_Classes_Morphisms_Prop.cm* theories/Classes/.coqnative/NCoq_Classes_Morphisms_Relations.cm* theories/Classes/.coqnative/NCoq_Classes_RelationClasses.cm* theories/Classes/.coqnative/NCoq_Classes_RelationPairs.cm* theories/Classes/.coqnative/NCoq_Classes_SetoidClass.cm* theories/Classes/.coqnative/NCoq_Classes_SetoidDec.cm* theories/Classes/.coqnative/NCoq_Classes_SetoidTactics.cm* theories/Compat/.coqnative/NCoq_Compat_AdmitAxiom.cm* theories/Compat/.coqnative/NCoq_Compat_Coq810.cm* theories/Compat/.coqnative/NCoq_Compat_Coq811.cm* theories/Compat/.coqnative/NCoq_Compat_Coq812.cm* theories/FSets/.coqnative/NCoq_FSets_FMapAVL.cm* theories/FSets/.coqnative/NCoq_FSets_FMapFacts.cm* theories/FSets/.coqnative/NCoq_FSets_FMapFullAVL.cm* theories/FSets/.coqnative/NCoq_FSets_FMapInterface.cm* theories/FSets/.coqnative/NCoq_FSets_FMapList.cm* theories/FSets/.coqnative/NCoq_FSets_FMapPositive.cm* theories/FSets/.coqnative/NCoq_FSets_FMapWeakList.cm* theories/FSets/.coqnative/NCoq_FSets_FMaps.cm* theories/FSets/.coqnative/NCoq_FSets_FSetAVL.cm* theories/FSets/.coqnative/NCoq_FSets_FSetBridge.cm* theories/FSets/.coqnative/NCoq_FSets_FSetCompat.cm* theories/FSets/.coqnative/NCoq_FSets_FSetDecide.cm* theories/FSets/.coqnative/NCoq_FSets_FSetEqProperties.cm* theories/FSets/.coqnative/NCoq_FSets_FSetFacts.cm* theories/FSets/.coqnative/NCoq_FSets_FSetInterface.cm* theories/FSets/.coqnative/NCoq_FSets_FSetList.cm* theories/FSets/.coqnative/NCoq_FSets_FSetPositive.cm* theories/FSets/.coqnative/NCoq_FSets_FSetProperties.cm* theories/FSets/.coqnative/NCoq_FSets_FSetToFiniteSet.cm* theories/FSets/.coqnative/NCoq_FSets_FSetWeakList.cm* theories/FSets/.coqnative/NCoq_FSets_FSets.cm* theories/Floats/.coqnative/NCoq_Floats_FloatAxioms.cm* theories/Floats/.coqnative/NCoq_Floats_FloatClass.cm* theories/Floats/.coqnative/NCoq_Floats_FloatLemmas.cm* theories/Floats/.coqnative/NCoq_Floats_FloatOps.cm* theories/Floats/.coqnative/NCoq_Floats_Floats.cm* theories/Floats/.coqnative/NCoq_Floats_PrimFloat.cm* theories/Floats/.coqnative/NCoq_Floats_SpecFloat.cm* theories/Init/.coqnative/NCoq_Init_Byte.cm* theories/Init/.coqnative/NCoq_Init_Datatypes.cm* theories/Init/.coqnative/NCoq_Init_Decimal.cm* theories/Init/.coqnative/NCoq_Init_Hexadecimal.cm* theories/Init/.coqnative/NCoq_Init_Logic.cm* theories/Init/.coqnative/NCoq_Init_Logic_Type.cm* theories/Init/.coqnative/NCoq_Init_Ltac.cm* theories/Init/.coqnative/NCoq_Init_Nat.cm* theories/Init/.coqnative/NCoq_Init_Notations.cm* theories/Init/.coqnative/NCoq_Init_Numeral.cm* theories/Init/.coqnative/NCoq_Init_Peano.cm* theories/Init/.coqnative/NCoq_Init_Prelude.cm* theories/Init/.coqnative/NCoq_Init_Specif.cm* theories/Init/.coqnative/NCoq_Init_Tactics.cm* theories/Init/.coqnative/NCoq_Init_Tauto.cm* theories/Init/.coqnative/NCoq_Init_Wf.cm* theories/Lists/.coqnative/NCoq_Lists_List.cm* theories/Lists/.coqnative/NCoq_Lists_ListDec.cm* theories/Lists/.coqnative/NCoq_Lists_ListSet.cm* theories/Lists/.coqnative/NCoq_Lists_ListTactics.cm* theories/Lists/.coqnative/NCoq_Lists_SetoidList.cm* theories/Lists/.coqnative/NCoq_Lists_SetoidPermutation.cm* theories/Lists/.coqnative/NCoq_Lists_StreamMemo.cm* theories/Lists/.coqnative/NCoq_Lists_Streams.cm* theories/Logic/.coqnative/NCoq_Logic_Berardi.cm* theories/Logic/.coqnative/NCoq_Logic_ChoiceFacts.cm* theories/Logic/.coqnative/NCoq_Logic_Classical.cm* theories/Logic/.coqnative/NCoq_Logic_ClassicalChoice.cm* theories/Logic/.coqnative/NCoq_Logic_ClassicalDescription.cm* theories/Logic/.coqnative/NCoq_Logic_ClassicalEpsilon.cm* theories/Logic/.coqnative/NCoq_Logic_ClassicalFacts.cm* theories/Logic/.coqnative/NCoq_Logic_ClassicalUniqueChoice.cm* theories/Logic/.coqnative/NCoq_Logic_Classical_Pred_Type.cm* theories/Logic/.coqnative/NCoq_Logic_Classical_Prop.cm* theories/Logic/.coqnative/NCoq_Logic_ConstructiveEpsilon.cm* theories/Logic/.coqnative/NCoq_Logic_Decidable.cm* theories/Logic/.coqnative/NCoq_Logic_Description.cm* theories/Logic/.coqnative/NCoq_Logic_Diaconescu.cm* theories/Logic/.coqnative/NCoq_Logic_Epsilon.cm* theories/Logic/.coqnative/NCoq_Logic_Eqdep.cm* theories/Logic/.coqnative/NCoq_Logic_EqdepFacts.cm* theories/Logic/.coqnative/NCoq_Logic_Eqdep_dec.cm* theories/Logic/.coqnative/NCoq_Logic_ExtensionalityFacts.cm* theories/Logic/.coqnative/NCoq_Logic_ExtensionalFunctionRepresentative.cm* theories/Logic/.coqnative/NCoq_Logic_FinFun.cm* theories/Logic/.coqnative/NCoq_Logic_FunctionalExtensionality.cm* theories/Logic/.coqnative/NCoq_Logic_HLevels.cm* theories/Logic/.coqnative/NCoq_Logic_Hurkens.cm* theories/Logic/.coqnative/NCoq_Logic_IndefiniteDescription.cm* theories/Logic/.coqnative/NCoq_Logic_JMeq.cm* theories/Logic/.coqnative/NCoq_Logic_ProofIrrelevance.cm* theories/Logic/.coqnative/NCoq_Logic_ProofIrrelevanceFacts.cm* theories/Logic/.coqnative/NCoq_Logic_PropExtensionality.cm* theories/Logic/.coqnative/NCoq_Logic_PropExtensionalityFacts.cm* theories/Logic/.coqnative/NCoq_Logic_PropFacts.cm* theories/Logic/.coqnative/NCoq_Logic_RelationalChoice.cm* theories/Logic/.coqnative/NCoq_Logic_SetIsType.cm* theories/Logic/.coqnative/NCoq_Logic_SetoidChoice.cm* theories/Logic/.coqnative/NCoq_Logic_StrictProp.cm* theories/Logic/.coqnative/NCoq_Logic_WKL.cm* theories/Logic/.coqnative/NCoq_Logic_WeakFan.cm* theories/MSets/.coqnative/NCoq_MSets_MSetAVL.cm* theories/MSets/.coqnative/NCoq_MSets_MSetDecide.cm* theories/MSets/.coqnative/NCoq_MSets_MSetEqProperties.cm* theories/MSets/.coqnative/NCoq_MSets_MSetFacts.cm* theories/MSets/.coqnative/NCoq_MSets_MSetGenTree.cm* theories/MSets/.coqnative/NCoq_MSets_MSetInterface.cm* theories/MSets/.coqnative/NCoq_MSets_MSetList.cm* theories/MSets/.coqnative/NCoq_MSets_MSetPositive.cm* theories/MSets/.coqnative/NCoq_MSets_MSetProperties.cm* theories/MSets/.coqnative/NCoq_MSets_MSetRBT.cm* theories/MSets/.coqnative/NCoq_MSets_MSetToFiniteSet.cm* theories/MSets/.coqnative/NCoq_MSets_MSetWeakList.cm* theories/MSets/.coqnative/NCoq_MSets_MSets.cm* theories/NArith/.coqnative/NCoq_NArith_BinNat.cm* theories/NArith/.coqnative/NCoq_NArith_BinNatDef.cm* theories/NArith/.coqnative/NCoq_NArith_NArith.cm* theories/NArith/.coqnative/NCoq_NArith_Ndec.cm* theories/NArith/.coqnative/NCoq_NArith_Ndigits.cm* theories/NArith/.coqnative/NCoq_NArith_Ndist.cm* theories/NArith/.coqnative/NCoq_NArith_Ndiv_def.cm* theories/NArith/.coqnative/NCoq_NArith_Ngcd_def.cm* theories/NArith/.coqnative/NCoq_NArith_Nnat.cm* theories/NArith/.coqnative/NCoq_NArith_Nsqrt_def.cm* theories/Numbers/.coqnative/NCoq_Numbers_AltBinNotations.cm* theories/Numbers/.coqnative/NCoq_Numbers_BinNums.cm* theories/Numbers/Cyclic/Abstract/.coqnative/NCoq_Numbers_Cyclic_Abstract_CyclicAxioms.cm* theories/Numbers/Cyclic/Abstract/.coqnative/NCoq_Numbers_Cyclic_Abstract_DoubleType.cm* theories/Numbers/Cyclic/Abstract/.coqnative/NCoq_Numbers_Cyclic_Abstract_NZCyclic.cm* theories/Numbers/Cyclic/Int31/.coqnative/NCoq_Numbers_Cyclic_Int31_Cyclic31.cm* theories/Numbers/Cyclic/Int31/.coqnative/NCoq_Numbers_Cyclic_Int31_Int31.cm* theories/Numbers/Cyclic/Int31/.coqnative/NCoq_Numbers_Cyclic_Int31_Ring31.cm* theories/Numbers/Cyclic/Int63/.coqnative/NCoq_Numbers_Cyclic_Int63_Cyclic63.cm* theories/Numbers/Cyclic/Int63/.coqnative/NCoq_Numbers_Cyclic_Int63_Int63.cm* theories/Numbers/Cyclic/Int63/.coqnative/NCoq_Numbers_Cyclic_Int63_Ring63.cm* theories/Numbers/Cyclic/ZModulo/.coqnative/NCoq_Numbers_Cyclic_ZModulo_ZModulo.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalFacts.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalN.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalNat.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalPos.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalQ.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalString.cm* theories/Numbers/.coqnative/NCoq_Numbers_DecimalZ.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalFacts.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalN.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalNat.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalPos.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalQ.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalString.cm* theories/Numbers/.coqnative/NCoq_Numbers_HexadecimalZ.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZAdd.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZAddOrder.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZAxioms.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZBase.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZBits.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZDivEucl.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZDivFloor.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZDivTrunc.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZGcd.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZLcm.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZLt.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZMaxMin.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZMul.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZMulOrder.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZParity.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZPow.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZProperties.cm* theories/Numbers/Integer/Abstract/.coqnative/NCoq_Numbers_Integer_Abstract_ZSgnAbs.cm* theories/Numbers/Integer/Binary/.coqnative/NCoq_Numbers_Integer_Binary_ZBinary.cm* theories/Numbers/Integer/NatPairs/.coqnative/NCoq_Numbers_Integer_NatPairs_ZNatPairs.cm* theories/Numbers/.coqnative/NCoq_Numbers_NaryFunctions.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZAdd.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZAddOrder.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZAxioms.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZBase.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZBits.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZDiv.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZDomain.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZGcd.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZLog.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZMul.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZMulOrder.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZOrder.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZParity.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZPow.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZProperties.cm* theories/Numbers/NatInt/.coqnative/NCoq_Numbers_NatInt_NZSqrt.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NAdd.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NAddOrder.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NAxioms.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NBase.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NBits.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NDefOps.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NDiv.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NGcd.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NIso.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NLcm.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NLog.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NMaxMin.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NMulOrder.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NOrder.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NParity.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NPow.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NProperties.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NSqrt.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NStrongRec.cm* theories/Numbers/Natural/Abstract/.coqnative/NCoq_Numbers_Natural_Abstract_NSub.cm* theories/Numbers/Natural/Binary/.coqnative/NCoq_Numbers_Natural_Binary_NBinary.cm* theories/Numbers/Natural/Peano/.coqnative/NCoq_Numbers_Natural_Peano_NPeano.cm* theories/Numbers/.coqnative/NCoq_Numbers_NumPrelude.cm* theories/PArith/.coqnative/NCoq_PArith_BinPos.cm* theories/PArith/.coqnative/NCoq_PArith_BinPosDef.cm* theories/PArith/.coqnative/NCoq_PArith_PArith.cm* theories/PArith/.coqnative/NCoq_PArith_POrderedType.cm* theories/PArith/.coqnative/NCoq_PArith_Pnat.cm* theories/Program/.coqnative/NCoq_Program_Basics.cm* theories/Program/.coqnative/NCoq_Program_Combinators.cm* theories/Program/.coqnative/NCoq_Program_Equality.cm* theories/Program/.coqnative/NCoq_Program_Program.cm* theories/Program/.coqnative/NCoq_Program_Subset.cm* theories/Program/.coqnative/NCoq_Program_Syntax.cm* theories/Program/.coqnative/NCoq_Program_Tactics.cm* theories/Program/.coqnative/NCoq_Program_Utils.cm* theories/Program/.coqnative/NCoq_Program_Wf.cm* theories/QArith/.coqnative/NCoq_QArith_QArith.cm* theories/QArith/.coqnative/NCoq_QArith_QArith_base.cm* theories/QArith/.coqnative/NCoq_QArith_QOrderedType.cm* theories/QArith/.coqnative/NCoq_QArith_Qabs.cm* theories/QArith/.coqnative/NCoq_QArith_Qcabs.cm* theories/QArith/.coqnative/NCoq_QArith_Qcanon.cm* theories/QArith/.coqnative/NCoq_QArith_Qfield.cm* theories/QArith/.coqnative/NCoq_QArith_Qminmax.cm* theories/QArith/.coqnative/NCoq_QArith_Qpower.cm* theories/QArith/.coqnative/NCoq_QArith_Qreals.cm* theories/QArith/.coqnative/NCoq_QArith_Qreduction.cm* theories/QArith/.coqnative/NCoq_QArith_Qring.cm* theories/QArith/.coqnative/NCoq_QArith_Qround.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveAbs.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveLUB.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveLimits.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveMinMax.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructivePower.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveReals.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveRealsMorphisms.cm* theories/Reals/Abstract/.coqnative/NCoq_Reals_Abstract_ConstructiveSum.cm* theories/Reals/.coqnative/NCoq_Reals_Alembert.cm* theories/Reals/.coqnative/NCoq_Reals_AltSeries.cm* theories/Reals/.coqnative/NCoq_Reals_ArithProp.cm* theories/Reals/.coqnative/NCoq_Reals_Binomial.cm* theories/Reals/Cauchy/.coqnative/NCoq_Reals_Cauchy_ConstructiveCauchyAbs.cm* theories/Reals/Cauchy/.coqnative/NCoq_Reals_Cauchy_ConstructiveCauchyReals.cm* theories/Reals/Cauchy/.coqnative/NCoq_Reals_Cauchy_ConstructiveCauchyRealsMult.cm* theories/Reals/Cauchy/.coqnative/NCoq_Reals_Cauchy_ConstructiveRcomplete.cm* theories/Reals/.coqnative/NCoq_Reals_Cauchy_prod.cm* theories/Reals/.coqnative/NCoq_Reals_ClassicalConstructiveReals.cm* theories/Reals/.coqnative/NCoq_Reals_ClassicalDedekindReals.cm* theories/Reals/.coqnative/NCoq_Reals_Cos_plus.cm* theories/Reals/.coqnative/NCoq_Reals_Cos_rel.cm* theories/Reals/.coqnative/NCoq_Reals_DiscrR.cm* theories/Reals/.coqnative/NCoq_Reals_Exp_prop.cm* theories/Reals/.coqnative/NCoq_Reals_Integration.cm* theories/Reals/.coqnative/NCoq_Reals_MVT.cm* theories/Reals/.coqnative/NCoq_Reals_Machin.cm* theories/Reals/.coqnative/NCoq_Reals_NewtonInt.cm* theories/Reals/.coqnative/NCoq_Reals_PSeries_reg.cm* theories/Reals/.coqnative/NCoq_Reals_PartSum.cm* theories/Reals/.coqnative/NCoq_Reals_RIneq.cm* theories/Reals/.coqnative/NCoq_Reals_RList.cm* theories/Reals/.coqnative/NCoq_Reals_ROrderedType.cm* theories/Reals/.coqnative/NCoq_Reals_R_Ifp.cm* theories/Reals/.coqnative/NCoq_Reals_R_sqr.cm* theories/Reals/.coqnative/NCoq_Reals_R_sqrt.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis1.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis2.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis3.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis4.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis5.cm* theories/Reals/.coqnative/NCoq_Reals_Ranalysis_reg.cm* theories/Reals/.coqnative/NCoq_Reals_Ratan.cm* theories/Reals/.coqnative/NCoq_Reals_Raxioms.cm* theories/Reals/.coqnative/NCoq_Reals_Rbase.cm* theories/Reals/.coqnative/NCoq_Reals_Rbasic_fun.cm* theories/Reals/.coqnative/NCoq_Reals_Rcomplete.cm* theories/Reals/.coqnative/NCoq_Reals_Rdefinitions.cm* theories/Reals/.coqnative/NCoq_Reals_Rderiv.cm* theories/Reals/.coqnative/NCoq_Reals_Reals.cm* theories/Reals/.coqnative/NCoq_Reals_Rfunctions.cm* theories/Reals/.coqnative/NCoq_Reals_Rgeom.cm* theories/Reals/.coqnative/NCoq_Reals_RiemannInt.cm* theories/Reals/.coqnative/NCoq_Reals_RiemannInt_SF.cm* theories/Reals/.coqnative/NCoq_Reals_Rlimit.cm* theories/Reals/.coqnative/NCoq_Reals_Rlogic.cm* theories/Reals/.coqnative/NCoq_Reals_Rminmax.cm* theories/Reals/.coqnative/NCoq_Reals_Rpow_def.cm* theories/Reals/.coqnative/NCoq_Reals_Rpower.cm* theories/Reals/.coqnative/NCoq_Reals_Rprod.cm* theories/Reals/.coqnative/NCoq_Reals_Rregisternames.cm* theories/Reals/.coqnative/NCoq_Reals_Rseries.cm* theories/Reals/.coqnative/NCoq_Reals_Rsigma.cm* theories/Reals/.coqnative/NCoq_Reals_Rsqrt_def.cm* theories/Reals/.coqnative/NCoq_Reals_Rtopology.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo1.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_alt.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_calc.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_def.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_facts.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_fun.cm* theories/Reals/.coqnative/NCoq_Reals_Rtrigo_reg.cm* theories/Reals/.coqnative/NCoq_Reals_Runcountable.cm* theories/Reals/.coqnative/NCoq_Reals_SeqProp.cm* theories/Reals/.coqnative/NCoq_Reals_SeqSeries.cm* theories/Reals/.coqnative/NCoq_Reals_SplitAbsolu.cm* theories/Reals/.coqnative/NCoq_Reals_SplitRmult.cm* theories/Reals/.coqnative/NCoq_Reals_Sqrt_reg.cm* theories/Relations/.coqnative/NCoq_Relations_Operators_Properties.cm* theories/Relations/.coqnative/NCoq_Relations_Relation_Definitions.cm* theories/Relations/.coqnative/NCoq_Relations_Relation_Operators.cm* theories/Relations/.coqnative/NCoq_Relations_Relations.cm* theories/Setoids/.coqnative/NCoq_Setoids_Setoid.cm* theories/Sets/.coqnative/NCoq_Sets_Classical_sets.cm* theories/Sets/.coqnative/NCoq_Sets_Constructive_sets.cm* theories/Sets/.coqnative/NCoq_Sets_Cpo.cm* theories/Sets/.coqnative/NCoq_Sets_Ensembles.cm* theories/Sets/.coqnative/NCoq_Sets_Finite_sets.cm* theories/Sets/.coqnative/NCoq_Sets_Finite_sets_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Image.cm* theories/Sets/.coqnative/NCoq_Sets_Infinite_sets.cm* theories/Sets/.coqnative/NCoq_Sets_Integers.cm* theories/Sets/.coqnative/NCoq_Sets_Multiset.cm* theories/Sets/.coqnative/NCoq_Sets_Partial_Order.cm* theories/Sets/.coqnative/NCoq_Sets_Permut.cm* theories/Sets/.coqnative/NCoq_Sets_Powerset.cm* theories/Sets/.coqnative/NCoq_Sets_Powerset_Classical_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Powerset_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_1.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_1_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_2.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_2_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_3.cm* theories/Sets/.coqnative/NCoq_Sets_Relations_3_facts.cm* theories/Sets/.coqnative/NCoq_Sets_Uniset.cm* theories/Sorting/.coqnative/NCoq_Sorting_CPermutation.cm* theories/Sorting/.coqnative/NCoq_Sorting_Heap.cm* theories/Sorting/.coqnative/NCoq_Sorting_Mergesort.cm* theories/Sorting/.coqnative/NCoq_Sorting_PermutEq.cm* theories/Sorting/.coqnative/NCoq_Sorting_PermutSetoid.cm* theories/Sorting/.coqnative/NCoq_Sorting_Permutation.cm* theories/Sorting/.coqnative/NCoq_Sorting_Sorted.cm* theories/Sorting/.coqnative/NCoq_Sorting_Sorting.cm* theories/Strings/.coqnative/NCoq_Strings_Ascii.cm* theories/Strings/.coqnative/NCoq_Strings_BinaryString.cm* theories/Strings/.coqnative/NCoq_Strings_Byte.cm* theories/Strings/.coqnative/NCoq_Strings_ByteVector.cm* theories/Strings/.coqnative/NCoq_Strings_HexString.cm* theories/Strings/.coqnative/NCoq_Strings_OctalString.cm* theories/Strings/.coqnative/NCoq_Strings_String.cm* theories/Structures/.coqnative/NCoq_Structures_DecidableType.cm* theories/Structures/.coqnative/NCoq_Structures_DecidableTypeEx.cm* theories/Structures/.coqnative/NCoq_Structures_Equalities.cm* theories/Structures/.coqnative/NCoq_Structures_EqualitiesFacts.cm* theories/Structures/.coqnative/NCoq_Structures_GenericMinMax.cm* theories/Structures/.coqnative/NCoq_Structures_OrderedType.cm* theories/Structures/.coqnative/NCoq_Structures_OrderedTypeAlt.cm* theories/Structures/.coqnative/NCoq_Structures_OrderedTypeEx.cm* theories/Structures/.coqnative/NCoq_Structures_Orders.cm* theories/Structures/.coqnative/NCoq_Structures_OrdersAlt.cm* theories/Structures/.coqnative/NCoq_Structures_OrdersEx.cm* theories/Structures/.coqnative/NCoq_Structures_OrdersFacts.cm* theories/Structures/.coqnative/NCoq_Structures_OrdersLists.cm* theories/Structures/.coqnative/NCoq_Structures_OrdersTac.cm* theories/Unicode/.coqnative/NCoq_Unicode_Utf8.cm* theories/Unicode/.coqnative/NCoq_Unicode_Utf8_core.cm* theories/Vectors/.coqnative/NCoq_Vectors_Fin.cm* theories/Vectors/.coqnative/NCoq_Vectors_Vector.cm* theories/Vectors/.coqnative/NCoq_Vectors_VectorDef.cm* theories/Vectors/.coqnative/NCoq_Vectors_VectorEq.cm* theories/Vectors/.coqnative/NCoq_Vectors_VectorSpec.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Disjoint_Union.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Inclusion.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Inverse_Image.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Lexicographic_Exponentiation.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Lexicographic_Product.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Transitive_Closure.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Union.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Well_Ordering.cm* theories/Wellfounded/.coqnative/NCoq_Wellfounded_Wellfounded.cm* theories/ZArith/.coqnative/NCoq_ZArith_BinInt.cm* theories/ZArith/.coqnative/NCoq_ZArith_BinIntDef.cm* theories/ZArith/.coqnative/NCoq_ZArith_Int.cm* theories/ZArith/.coqnative/NCoq_ZArith_Wf_Z.cm* theories/ZArith/.coqnative/NCoq_ZArith_ZArith.cm* theories/ZArith/.coqnative/NCoq_ZArith_ZArith_base.cm* theories/ZArith/.coqnative/NCoq_ZArith_ZArith_dec.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zabs.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zbool.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zcompare.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zcomplements.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zdigits.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zdiv.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zeuclid.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zeven.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zgcd_alt.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zhints.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zmax.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zmin.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zminmax.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zmisc.cm* theories/ZArith/.coqnative/NCoq_ZArith_Znat.cm* theories/ZArith/.coqnative/NCoq_ZArith_Znumtheory.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zorder.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zpow_alt.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zpow_def.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zpow_facts.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zpower.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zquot.cm* theories/ZArith/.coqnative/NCoq_ZArith_Zwf.cm* theories/ZArith/.coqnative/NCoq_ZArith_auxiliary.cm* theories/btauto/.coqnative/NCoq_btauto_Algebra.cm* theories/btauto/.coqnative/NCoq_btauto_Btauto.cm* theories/btauto/.coqnative/NCoq_btauto_Reflect.cm* theories/derive/.coqnative/NCoq_derive_Derive.cm* theories/ssr/.coqnative/NCoq_ssr_ssrbool.cm* theories/ssr/.coqnative/NCoq_ssr_ssrclasses.cm* theories/ssr/.coqnative/NCoq_ssr_ssreflect.cm* theories/ssr/.coqnative/NCoq_ssr_ssrfun.cm* theories/ssr/.coqnative/NCoq_ssr_ssrsetoid.cm* theories/ssr/.coqnative/NCoq_ssr_ssrunder.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellBasic.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatInt.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatInteger.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatNum.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellString.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellZInt.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellZInteger.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrHaskellZNum.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOCamlFloats.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOCamlInt63.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlBasic.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlBigIntConv.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlChar.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlIntConv.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlNatBigInt.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlNatInt.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlString.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlNativeString.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlZBigInt.cm* theories/extraction/.coqnative/NCoq_extraction_ExtrOcamlZInt.cm* theories/extraction/.coqnative/NCoq_extraction_Extraction.cm* theories/funind/.coqnative/NCoq_funind_FunInd.cm* theories/funind/.coqnative/NCoq_funind_Recdef.cm* theories/micromega/.coqnative/NCoq_micromega_DeclConstant.cm* theories/micromega/.coqnative/NCoq_micromega_Env.cm* theories/micromega/.coqnative/NCoq_micromega_EnvRing.cm* theories/micromega/.coqnative/NCoq_micromega_Fourier.cm* theories/micromega/.coqnative/NCoq_micromega_Fourier_util.cm* theories/micromega/.coqnative/NCoq_micromega_Lia.cm* theories/micromega/.coqnative/NCoq_micromega_Lqa.cm* theories/micromega/.coqnative/NCoq_micromega_Lra.cm* theories/micromega/.coqnative/NCoq_micromega_MExtraction.cm* theories/micromega/.coqnative/NCoq_micromega_OrderedRing.cm* theories/micromega/.coqnative/NCoq_micromega_Psatz.cm* theories/micromega/.coqnative/NCoq_micromega_QMicromega.cm* theories/micromega/.coqnative/NCoq_micromega_RMicromega.cm* theories/micromega/.coqnative/NCoq_micromega_Refl.cm* theories/micromega/.coqnative/NCoq_micromega_RingMicromega.cm* theories/micromega/.coqnative/NCoq_micromega_Tauto.cm* theories/micromega/.coqnative/NCoq_micromega_VarMap.cm* theories/micromega/.coqnative/NCoq_micromega_ZArith_hints.cm* theories/micromega/.coqnative/NCoq_micromega_ZCoeff.cm* theories/micromega/.coqnative/NCoq_micromega_ZMicromega.cm* theories/micromega/.coqnative/NCoq_micromega_Zify.cm* theories/micromega/.coqnative/NCoq_micromega_ZifyBool.cm* theories/micromega/.coqnative/NCoq_micromega_ZifyClasses.cm* theories/micromega/.coqnative/NCoq_micromega_ZifyInst.cm* theories/micromega/.coqnative/NCoq_micromega_ZifyComparison.cm* theories/micromega/.coqnative/NCoq_micromega_ZifyPow.cm* theories/micromega/.coqnative/NCoq_micromega_Ztac.cm* theories/nsatz/.coqnative/NCoq_nsatz_Nsatz.cm* theories/nsatz/.coqnative/NCoq_nsatz_NsatzTactic.cm* theories/omega/.coqnative/NCoq_omega_Omega.cm* theories/omega/.coqnative/NCoq_omega_OmegaLemmas.cm* theories/omega/.coqnative/NCoq_omega_OmegaPlugin.cm* theories/omega/.coqnative/NCoq_omega_OmegaTactic.cm* theories/omega/.coqnative/NCoq_omega_PreOmega.cm* theories/rtauto/.coqnative/NCoq_rtauto_Bintree.cm* theories/rtauto/.coqnative/NCoq_rtauto_Rtauto.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Algebra_syntax.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_ArithRing.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_BinList.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Cring.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Field.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Field_tac.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Field_theory.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_InitialRing.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Integral_domain.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_NArithRing.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_initial.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_polynom.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_tac.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_RealField.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ring.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_base.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_polynom.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_tac.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_theory.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_Q.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_R.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_Z.cm* theories/setoid_ring/.coqnative/NCoq_setoid_ring_ZArithRing.cm* theories/ssrmatching/.coqnative/NCoq_ssrmatching_ssrmatching.cm* theories/ssrsearch/.coqnative/NCoq_ssrsearch_ssrsearch.cm* usercontrib/Ltac2/.coqnative/NLtac2_Array.cm* usercontrib/Ltac2/.coqnative/NLtac2_Bool.cm* usercontrib/Ltac2/.coqnative/NLtac2_Char.cm* usercontrib/Ltac2/.coqnative/NLtac2_Constr.cm* usercontrib/Ltac2/.coqnative/NLtac2_Control.cm* usercontrib/Ltac2/.coqnative/NLtac2_Env.cm* usercontrib/Ltac2/.coqnative/NLtac2_Fresh.cm* usercontrib/Ltac2/.coqnative/NLtac2_Ident.cm* usercontrib/Ltac2/.coqnative/NLtac2_Init.cm* usercontrib/Ltac2/.coqnative/NLtac2_Int.cm* usercontrib/Ltac2/.coqnative/NLtac2_List.cm* usercontrib/Ltac2/.coqnative/NLtac2_Ltac1.cm* usercontrib/Ltac2/.coqnative/NLtac2_Ltac2.cm* usercontrib/Ltac2/.coqnative/NLtac2_Message.cm* usercontrib/Ltac2/.coqnative/NLtac2_Notations.cm* usercontrib/Ltac2/.coqnative/NLtac2_Option.cm* usercontrib/Ltac2/.coqnative/NLtac2_Pattern.cm* usercontrib/Ltac2/.coqnative/NLtac2_Std.cm* usercontrib/Ltac2/.coqnative/NLtac2_String.cm*  true
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" theories/Arith/Arith.v theories/Arith/Arith_base.v theories/Arith/Between.v theories/Arith/Bool_nat.v theories/Arith/Compare.v theories/Arith/Compare_dec.v theories/Arith/Div2.v theories/Arith/EqNat.v theories/Arith/Euclid.v theories/Arith/Even.v theories/Arith/Factorial.v theories/Arith/Gt.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Max.v theories/Arith/Min.v theories/Arith/Minus.v theories/Arith/Mult.v theories/Arith/PeanoNat.v theories/Arith/Peano_dec.v theories/Arith/Plus.v theories/Arith/Wf_nat.v theories/Bool/Bool.v theories/Bool/BoolEq.v theories/Bool/BoolOrder.v theories/Bool/Bvector.v theories/Bool/DecBool.v theories/Bool/IfProp.v theories/Bool/Sumbool.v theories/Bool/Zerob.v theories/Classes/CEquivalence.v theories/Classes/CMorphisms.v theories/Classes/CRelationClasses.v theories/Classes/DecidableClass.v theories/Classes/EquivDec.v theories/Classes/Equivalence.v theories/Classes/Init.v theories/Classes/Morphisms.v theories/Classes/Morphisms_Prop.v theories/Classes/Morphisms_Relations.v theories/Classes/RelationClasses.v theories/Classes/RelationPairs.v theories/Classes/SetoidClass.v theories/Classes/SetoidDec.v theories/Classes/SetoidTactics.v theories/Compat/AdmitAxiom.v theories/Compat/Coq810.v theories/Compat/Coq811.v theories/Compat/Coq812.v theories/FSets/FMapAVL.v theories/FSets/FMapFacts.v theories/FSets/FMapFullAVL.v theories/FSets/FMapInterface.v theories/FSets/FMapList.v theories/FSets/FMapPositive.v theories/FSets/FMapWeakList.v theories/FSets/FMaps.v theories/FSets/FSetAVL.v theories/FSets/FSetBridge.v theories/FSets/FSetCompat.v theories/FSets/FSetDecide.v theories/FSets/FSetEqProperties.v theories/FSets/FSetFacts.v theories/FSets/FSetInterface.v theories/FSets/FSetList.v theories/FSets/FSetPositive.v theories/FSets/FSetProperties.v theories/FSets/FSetToFiniteSet.v theories/FSets/FSetWeakList.v theories/FSets/FSets.v theories/Floats/FloatAxioms.v theories/Floats/FloatClass.v theories/Floats/FloatLemmas.v theories/Floats/FloatOps.v theories/Floats/Floats.v theories/Floats/PrimFloat.v theories/Floats/SpecFloat.v theories/Init/Byte.v theories/Init/Datatypes.v theories/Init/Decimal.v theories/Init/Hexadecimal.v theories/Init/Logic.v theories/Init/Logic_Type.v theories/Init/Ltac.v theories/Init/Nat.v theories/Init/Notations.v theories/Init/Numeral.v theories/Init/Peano.v theories/Init/Prelude.v theories/Init/Specif.v theories/Init/Tactics.v theories/Init/Tauto.v theories/Init/Wf.v theories/Lists/List.v theories/Lists/ListDec.v theories/Lists/ListSet.v theories/Lists/ListTactics.v theories/Lists/SetoidList.v theories/Lists/SetoidPermutation.v theories/Lists/StreamMemo.v theories/Lists/Streams.v theories/Logic/Berardi.v theories/Logic/ChoiceFacts.v theories/Logic/Classical.v theories/Logic/ClassicalChoice.v theories/Logic/ClassicalDescription.v theories/Logic/ClassicalEpsilon.v theories/Logic/ClassicalFacts.v theories/Logic/ClassicalUniqueChoice.v theories/Logic/Classical_Pred_Type.v theories/Logic/Classical_Prop.v theories/Logic/ConstructiveEpsilon.v theories/Logic/Decidable.v theories/Logic/Description.v theories/Logic/Diaconescu.v theories/Logic/Epsilon.v theories/Logic/Eqdep.v theories/Logic/EqdepFacts.v theories/Logic/Eqdep_dec.v theories/Logic/ExtensionalityFacts.v theories/Logic/ExtensionalFunctionRepresentative.v theories/Logic/FinFun.v theories/Logic/FunctionalExtensionality.v theories/Logic/HLevels.v theories/Logic/Hurkens.v theories/Logic/IndefiniteDescription.v theories/Logic/JMeq.v theories/Logic/ProofIrrelevance.v theories/Logic/ProofIrrelevanceFacts.v theories/Logic/PropExtensionality.v theories/Logic/PropExtensionalityFacts.v theories/Logic/PropFacts.v theories/Logic/RelationalChoice.v theories/Logic/SetIsType.v theories/Logic/SetoidChoice.v theories/Logic/StrictProp.v theories/Logic/WKL.v theories/Logic/WeakFan.v theories/MSets/MSetAVL.v theories/MSets/MSetDecide.v theories/MSets/MSetEqProperties.v theories/MSets/MSetFacts.v theories/MSets/MSetGenTree.v theories/MSets/MSetInterface.v theories/MSets/MSetList.v theories/MSets/MSetPositive.v theories/MSets/MSetProperties.v theories/MSets/MSetRBT.v theories/MSets/MSetToFiniteSet.v theories/MSets/MSetWeakList.v theories/MSets/MSets.v theories/NArith/BinNat.v theories/NArith/BinNatDef.v theories/NArith/NArith.v theories/NArith/Ndec.v theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndiv_def.v theories/NArith/Ngcd_def.v theories/NArith/Nnat.v theories/NArith/Nsqrt_def.v theories/Numbers/AltBinNotations.v theories/Numbers/BinNums.v theories/Numbers/Cyclic/Abstract/CyclicAxioms.v theories/Numbers/Cyclic/Abstract/DoubleType.v theories/Numbers/Cyclic/Abstract/NZCyclic.v theories/Numbers/Cyclic/Int31/Cyclic31.v theories/Numbers/Cyclic/Int31/Int31.v theories/Numbers/Cyclic/Int31/Ring31.v theories/Numbers/Cyclic/Int63/Cyclic63.v theories/Numbers/Cyclic/Int63/Int63.v theories/Numbers/Cyclic/Int63/Ring63.v theories/Numbers/Cyclic/ZModulo/ZModulo.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalN.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v theories/Numbers/DecimalQ.v theories/Numbers/DecimalString.v theories/Numbers/DecimalZ.v theories/Numbers/HexadecimalFacts.v theories/Numbers/HexadecimalN.v theories/Numbers/HexadecimalNat.v theories/Numbers/HexadecimalPos.v theories/Numbers/HexadecimalQ.v theories/Numbers/HexadecimalString.v theories/Numbers/HexadecimalZ.v theories/Numbers/Integer/Abstract/ZAdd.v theories/Numbers/Integer/Abstract/ZAddOrder.v theories/Numbers/Integer/Abstract/ZAxioms.v theories/Numbers/Integer/Abstract/ZBase.v theories/Numbers/Integer/Abstract/ZBits.v theories/Numbers/Integer/Abstract/ZDivEucl.v theories/Numbers/Integer/Abstract/ZDivFloor.v theories/Numbers/Integer/Abstract/ZDivTrunc.v theories/Numbers/Integer/Abstract/ZGcd.v theories/Numbers/Integer/Abstract/ZLcm.v theories/Numbers/Integer/Abstract/ZLt.v theories/Numbers/Integer/Abstract/ZMaxMin.v theories/Numbers/Integer/Abstract/ZMul.v theories/Numbers/Integer/Abstract/ZMulOrder.v theories/Numbers/Integer/Abstract/ZParity.v theories/Numbers/Integer/Abstract/ZPow.v theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZSgnAbs.v theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v theories/Numbers/NaryFunctions.v theories/Numbers/NatInt/NZAdd.v theories/Numbers/NatInt/NZAddOrder.v theories/Numbers/NatInt/NZAxioms.v theories/Numbers/NatInt/NZBase.v theories/Numbers/NatInt/NZBits.v theories/Numbers/NatInt/NZDiv.v theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZGcd.v theories/Numbers/NatInt/NZLog.v theories/Numbers/NatInt/NZMul.v theories/Numbers/NatInt/NZMulOrder.v theories/Numbers/NatInt/NZOrder.v theories/Numbers/NatInt/NZParity.v theories/Numbers/NatInt/NZPow.v theories/Numbers/NatInt/NZProperties.v theories/Numbers/NatInt/NZSqrt.v theories/Numbers/Natural/Abstract/NAdd.v theories/Numbers/Natural/Abstract/NAddOrder.v theories/Numbers/Natural/Abstract/NAxioms.v theories/Numbers/Natural/Abstract/NBase.v theories/Numbers/Natural/Abstract/NBits.v theories/Numbers/Natural/Abstract/NDefOps.v theories/Numbers/Natural/Abstract/NDiv.v theories/Numbers/Natural/Abstract/NGcd.v theories/Numbers/Natural/Abstract/NIso.v theories/Numbers/Natural/Abstract/NLcm.v theories/Numbers/Natural/Abstract/NLog.v theories/Numbers/Natural/Abstract/NMaxMin.v theories/Numbers/Natural/Abstract/NMulOrder.v theories/Numbers/Natural/Abstract/NOrder.v theories/Numbers/Natural/Abstract/NParity.v theories/Numbers/Natural/Abstract/NPow.v theories/Numbers/Natural/Abstract/NProperties.v theories/Numbers/Natural/Abstract/NSqrt.v theories/Numbers/Natural/Abstract/NStrongRec.v theories/Numbers/Natural/Abstract/NSub.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v theories/Numbers/NumPrelude.v theories/PArith/BinPos.v theories/PArith/BinPosDef.v theories/PArith/PArith.v theories/PArith/POrderedType.v theories/PArith/Pnat.v theories/Program/Basics.v theories/Program/Combinators.v theories/Program/Equality.v theories/Program/Program.v theories/Program/Subset.v theories/Program/Syntax.v theories/Program/Tactics.v theories/Program/Utils.v theories/Program/Wf.v theories/QArith/QArith.v theories/QArith/QArith_base.v theories/QArith/QOrderedType.v theories/QArith/Qabs.v theories/QArith/Qcabs.v theories/QArith/Qcanon.v theories/QArith/Qfield.v theories/QArith/Qminmax.v theories/QArith/Qpower.v theories/QArith/Qreals.v theories/QArith/Qreduction.v theories/QArith/Qring.v theories/QArith/Qround.v theories/Reals/Abstract/ConstructiveAbs.v theories/Reals/Abstract/ConstructiveLUB.v theories/Reals/Abstract/ConstructiveLimits.v theories/Reals/Abstract/ConstructiveMinMax.v theories/Reals/Abstract/ConstructivePower.v theories/Reals/Abstract/ConstructiveReals.v theories/Reals/Abstract/ConstructiveRealsMorphisms.v theories/Reals/Abstract/ConstructiveSum.v theories/Reals/Alembert.v theories/Reals/AltSeries.v theories/Reals/ArithProp.v theories/Reals/Binomial.v theories/Reals/Cauchy/ConstructiveCauchyAbs.v theories/Reals/Cauchy/ConstructiveCauchyReals.v theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v theories/Reals/Cauchy/ConstructiveRcomplete.v theories/Reals/Cauchy_prod.v theories/Reals/ClassicalConstructiveReals.v theories/Reals/ClassicalDedekindReals.v theories/Reals/Cos_plus.v theories/Reals/Cos_rel.v theories/Reals/DiscrR.v theories/Reals/Exp_prop.v theories/Reals/Integration.v theories/Reals/MVT.v theories/Reals/Machin.v theories/Reals/NewtonInt.v theories/Reals/PSeries_reg.v theories/Reals/PartSum.v theories/Reals/RIneq.v theories/Reals/RList.v theories/Reals/ROrderedType.v theories/Reals/R_Ifp.v theories/Reals/R_sqr.v theories/Reals/R_sqrt.v theories/Reals/Ranalysis.v theories/Reals/Ranalysis1.v theories/Reals/Ranalysis2.v theories/Reals/Ranalysis3.v theories/Reals/Ranalysis4.v theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Ratan.v theories/Reals/Raxioms.v theories/Reals/Rbase.v theories/Reals/Rbasic_fun.v theories/Reals/Rcomplete.v theories/Reals/Rdefinitions.v theories/Reals/Rderiv.v theories/Reals/Reals.v theories/Reals/Rfunctions.v theories/Reals/Rgeom.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rlimit.v theories/Reals/Rlogic.v theories/Reals/Rminmax.v theories/Reals/Rpow_def.v theories/Reals/Rpower.v theories/Reals/Rprod.v theories/Reals/Rregisternames.v theories/Reals/Rseries.v theories/Reals/Rsigma.v theories/Reals/Rsqrt_def.v theories/Reals/Rtopology.v theories/Reals/Rtrigo.v theories/Reals/Rtrigo1.v theories/Reals/Rtrigo_alt.v theories/Reals/Rtrigo_calc.v theories/Reals/Rtrigo_def.v theories/Reals/Rtrigo_facts.v theories/Reals/Rtrigo_fun.v theories/Reals/Rtrigo_reg.v theories/Reals/Runcountable.v theories/Reals/SeqProp.v theories/Reals/SeqSeries.v theories/Reals/SplitAbsolu.v theories/Reals/SplitRmult.v theories/Reals/Sqrt_reg.v theories/Relations/Operators_Properties.v theories/Relations/Relation_Definitions.v theories/Relations/Relation_Operators.v theories/Relations/Relations.v theories/Setoids/Setoid.v theories/Sets/Classical_sets.v theories/Sets/Constructive_sets.v theories/Sets/Cpo.v theories/Sets/Ensembles.v theories/Sets/Finite_sets.v theories/Sets/Finite_sets_facts.v theories/Sets/Image.v theories/Sets/Infinite_sets.v theories/Sets/Integers.v theories/Sets/Multiset.v theories/Sets/Partial_Order.v theories/Sets/Permut.v theories/Sets/Powerset.v theories/Sets/Powerset_Classical_facts.v theories/Sets/Powerset_facts.v theories/Sets/Relations_1.v theories/Sets/Relations_1_facts.v theories/Sets/Relations_2.v theories/Sets/Relations_2_facts.v theories/Sets/Relations_3.v theories/Sets/Relations_3_facts.v theories/Sets/Uniset.v theories/Sorting/CPermutation.v theories/Sorting/Heap.v theories/Sorting/Mergesort.v theories/Sorting/PermutEq.v theories/Sorting/PermutSetoid.v theories/Sorting/Permutation.v theories/Sorting/Sorted.v theories/Sorting/Sorting.v theories/Strings/Ascii.v theories/Strings/BinaryString.v theories/Strings/Byte.v theories/Strings/ByteVector.v theories/Strings/HexString.v theories/Strings/OctalString.v theories/Strings/String.v theories/Structures/DecidableType.v theories/Structures/DecidableTypeEx.v theories/Structures/Equalities.v theories/Structures/EqualitiesFacts.v theories/Structures/GenericMinMax.v theories/Structures/OrderedType.v theories/Structures/OrderedTypeAlt.v theories/Structures/OrderedTypeEx.v theories/Structures/Orders.v theories/Structures/OrdersAlt.v theories/Structures/OrdersEx.v theories/Structures/OrdersFacts.v theories/Structures/OrdersLists.v theories/Structures/OrdersTac.v theories/Unicode/Utf8.v theories/Unicode/Utf8_core.v theories/Vectors/Fin.v theories/Vectors/Vector.v theories/Vectors/VectorDef.v theories/Vectors/VectorEq.v theories/Vectors/VectorSpec.v theories/Wellfounded/Disjoint_Union.v theories/Wellfounded/Inclusion.v theories/Wellfounded/Inverse_Image.v theories/Wellfounded/Lexicographic_Exponentiation.v theories/Wellfounded/Lexicographic_Product.v theories/Wellfounded/Transitive_Closure.v theories/Wellfounded/Union.v theories/Wellfounded/Well_Ordering.v theories/Wellfounded/Wellfounded.v theories/ZArith/BinInt.v theories/ZArith/BinIntDef.v theories/ZArith/Int.v theories/ZArith/Wf_Z.v theories/ZArith/ZArith.v theories/ZArith/ZArith_base.v theories/ZArith/ZArith_dec.v theories/ZArith/Zabs.v theories/ZArith/Zbool.v theories/ZArith/Zcompare.v theories/ZArith/Zcomplements.v theories/ZArith/Zdigits.v theories/ZArith/Zdiv.v theories/ZArith/Zeuclid.v theories/ZArith/Zeven.v theories/ZArith/Zgcd_alt.v theories/ZArith/Zhints.v theories/ZArith/Zmax.v theories/ZArith/Zmin.v theories/ZArith/Zminmax.v theories/ZArith/Zmisc.v theories/ZArith/Znat.v theories/ZArith/Znumtheory.v theories/ZArith/Zorder.v theories/ZArith/Zpow_alt.v theories/ZArith/Zpow_def.v theories/ZArith/Zpow_facts.v theories/ZArith/Zpower.v theories/ZArith/Zquot.v theories/ZArith/Zwf.v theories/ZArith/auxiliary.v theories/btauto/Algebra.v theories/btauto/Btauto.v theories/btauto/Reflect.v theories/derive/Derive.v theories/ssr/ssrbool.v theories/ssr/ssrclasses.v theories/ssr/ssreflect.v theories/ssr/ssrfun.v theories/ssr/ssrsetoid.v theories/ssr/ssrunder.v theories/extraction/ExtrHaskellBasic.v theories/extraction/ExtrHaskellNatInt.v theories/extraction/ExtrHaskellNatInteger.v theories/extraction/ExtrHaskellNatNum.v theories/extraction/ExtrHaskellString.v theories/extraction/ExtrHaskellZInt.v theories/extraction/ExtrHaskellZInteger.v theories/extraction/ExtrHaskellZNum.v theories/extraction/ExtrOCamlFloats.v theories/extraction/ExtrOCamlInt63.v theories/extraction/ExtrOcamlBasic.v theories/extraction/ExtrOcamlBigIntConv.v theories/extraction/ExtrOcamlChar.v theories/extraction/ExtrOcamlIntConv.v theories/extraction/ExtrOcamlNatBigInt.v theories/extraction/ExtrOcamlNatInt.v theories/extraction/ExtrOcamlString.v theories/extraction/ExtrOcamlNativeString.v theories/extraction/ExtrOcamlZBigInt.v theories/extraction/ExtrOcamlZInt.v theories/extraction/Extraction.v theories/funind/FunInd.v theories/funind/Recdef.v theories/micromega/DeclConstant.v theories/micromega/Env.v theories/micromega/EnvRing.v theories/micromega/Fourier.v theories/micromega/Fourier_util.v theories/micromega/Lia.v theories/micromega/Lqa.v theories/micromega/Lra.v theories/micromega/MExtraction.v theories/micromega/OrderedRing.v theories/micromega/Psatz.v theories/micromega/QMicromega.v theories/micromega/RMicromega.v theories/micromega/Refl.v theories/micromega/RingMicromega.v theories/micromega/Tauto.v theories/micromega/VarMap.v theories/micromega/ZArith_hints.v theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/Zify.v theories/micromega/ZifyBool.v theories/micromega/ZifyClasses.v theories/micromega/ZifyInst.v theories/micromega/ZifyComparison.v theories/micromega/ZifyPow.v theories/micromega/Ztac.v theories/nsatz/Nsatz.v theories/nsatz/NsatzTactic.v theories/omega/Omega.v theories/omega/OmegaLemmas.v theories/omega/OmegaPlugin.v theories/omega/OmegaTactic.v theories/omega/PreOmega.v theories/rtauto/Bintree.v theories/rtauto/Rtauto.v theories/setoid_ring/Algebra_syntax.v theories/setoid_ring/ArithRing.v theories/setoid_ring/BinList.v theories/setoid_ring/Cring.v theories/setoid_ring/Field.v theories/setoid_ring/Field_tac.v theories/setoid_ring/Field_theory.v theories/setoid_ring/InitialRing.v theories/setoid_ring/Integral_domain.v theories/setoid_ring/NArithRing.v theories/setoid_ring/Ncring.v theories/setoid_ring/Ncring_initial.v theories/setoid_ring/Ncring_polynom.v theories/setoid_ring/Ncring_tac.v theories/setoid_ring/RealField.v theories/setoid_ring/Ring.v theories/setoid_ring/Ring_base.v theories/setoid_ring/Ring_polynom.v theories/setoid_ring/Ring_tac.v theories/setoid_ring/Ring_theory.v theories/setoid_ring/Rings_Q.v theories/setoid_ring/Rings_R.v theories/setoid_ring/Rings_Z.v theories/setoid_ring/ZArithRing.v theories/ssrmatching/ssrmatching.v theories/ssrsearch/ssrsearch.v usercontrib/Ltac2/Array.v usercontrib/Ltac2/Bool.v usercontrib/Ltac2/Char.v usercontrib/Ltac2/Constr.v usercontrib/Ltac2/Control.v usercontrib/Ltac2/Env.v usercontrib/Ltac2/Fresh.v usercontrib/Ltac2/Ident.v usercontrib/Ltac2/Init.v usercontrib/Ltac2/Int.v usercontrib/Ltac2/List.v usercontrib/Ltac2/Ltac1.v usercontrib/Ltac2/Ltac2.v usercontrib/Ltac2/Message.v usercontrib/Ltac2/Notations.v usercontrib/Ltac2/Option.v usercontrib/Ltac2/Pattern.v usercontrib/Ltac2/Std.v usercontrib/Ltac2/String.v
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" theories/Arith/Arith.glob theories/Arith/Arith_base.glob theories/Arith/Between.glob theories/Arith/Bool_nat.glob theories/Arith/Compare.glob theories/Arith/Compare_dec.glob theories/Arith/Div2.glob theories/Arith/EqNat.glob theories/Arith/Euclid.glob theories/Arith/Even.glob theories/Arith/Factorial.glob theories/Arith/Gt.glob theories/Arith/Le.glob theories/Arith/Lt.glob theories/Arith/Max.glob theories/Arith/Min.glob theories/Arith/Minus.glob theories/Arith/Mult.glob theories/Arith/PeanoNat.glob theories/Arith/Peano_dec.glob theories/Arith/Plus.glob theories/Arith/Wf_nat.glob theories/Bool/Bool.glob theories/Bool/BoolEq.glob theories/Bool/BoolOrder.glob theories/Bool/Bvector.glob theories/Bool/DecBool.glob theories/Bool/IfProp.glob theories/Bool/Sumbool.glob theories/Bool/Zerob.glob theories/Classes/CEquivalence.glob theories/Classes/CMorphisms.glob theories/Classes/CRelationClasses.glob theories/Classes/DecidableClass.glob theories/Classes/EquivDec.glob theories/Classes/Equivalence.glob theories/Classes/Init.glob theories/Classes/Morphisms.glob theories/Classes/Morphisms_Prop.glob theories/Classes/Morphisms_Relations.glob theories/Classes/RelationClasses.glob theories/Classes/RelationPairs.glob theories/Classes/SetoidClass.glob theories/Classes/SetoidDec.glob theories/Classes/SetoidTactics.glob theories/Compat/AdmitAxiom.glob theories/Compat/Coq810.glob theories/Compat/Coq811.glob theories/Compat/Coq812.glob theories/FSets/FMapAVL.glob theories/FSets/FMapFacts.glob theories/FSets/FMapFullAVL.glob theories/FSets/FMapInterface.glob theories/FSets/FMapList.glob theories/FSets/FMapPositive.glob theories/FSets/FMapWeakList.glob theories/FSets/FMaps.glob theories/FSets/FSetAVL.glob theories/FSets/FSetBridge.glob theories/FSets/FSetCompat.glob theories/FSets/FSetDecide.glob theories/FSets/FSetEqProperties.glob theories/FSets/FSetFacts.glob theories/FSets/FSetInterface.glob theories/FSets/FSetList.glob theories/FSets/FSetPositive.glob theories/FSets/FSetProperties.glob theories/FSets/FSetToFiniteSet.glob theories/FSets/FSetWeakList.glob theories/FSets/FSets.glob theories/Floats/FloatAxioms.glob theories/Floats/FloatClass.glob theories/Floats/FloatLemmas.glob theories/Floats/FloatOps.glob theories/Floats/Floats.glob theories/Floats/PrimFloat.glob theories/Floats/SpecFloat.glob theories/Init/Byte.glob theories/Init/Datatypes.glob theories/Init/Decimal.glob theories/Init/Hexadecimal.glob theories/Init/Logic.glob theories/Init/Logic_Type.glob theories/Init/Ltac.glob theories/Init/Nat.glob theories/Init/Notations.glob theories/Init/Numeral.glob theories/Init/Peano.glob theories/Init/Prelude.glob theories/Init/Specif.glob theories/Init/Tactics.glob theories/Init/Tauto.glob theories/Init/Wf.glob theories/Lists/List.glob theories/Lists/ListDec.glob theories/Lists/ListSet.glob theories/Lists/ListTactics.glob theories/Lists/SetoidList.glob theories/Lists/SetoidPermutation.glob theories/Lists/StreamMemo.glob theories/Lists/Streams.glob theories/Logic/Berardi.glob theories/Logic/ChoiceFacts.glob theories/Logic/Classical.glob theories/Logic/ClassicalChoice.glob theories/Logic/ClassicalDescription.glob theories/Logic/ClassicalEpsilon.glob theories/Logic/ClassicalFacts.glob theories/Logic/ClassicalUniqueChoice.glob theories/Logic/Classical_Pred_Type.glob theories/Logic/Classical_Prop.glob theories/Logic/ConstructiveEpsilon.glob theories/Logic/Decidable.glob theories/Logic/Description.glob theories/Logic/Diaconescu.glob theories/Logic/Epsilon.glob theories/Logic/Eqdep.glob theories/Logic/EqdepFacts.glob theories/Logic/Eqdep_dec.glob theories/Logic/ExtensionalityFacts.glob theories/Logic/ExtensionalFunctionRepresentative.glob theories/Logic/FinFun.glob theories/Logic/FunctionalExtensionality.glob theories/Logic/HLevels.glob theories/Logic/Hurkens.glob theories/Logic/IndefiniteDescription.glob theories/Logic/JMeq.glob theories/Logic/ProofIrrelevance.glob theories/Logic/ProofIrrelevanceFacts.glob theories/Logic/PropExtensionality.glob theories/Logic/PropExtensionalityFacts.glob theories/Logic/PropFacts.glob theories/Logic/RelationalChoice.glob theories/Logic/SetIsType.glob theories/Logic/SetoidChoice.glob theories/Logic/StrictProp.glob theories/Logic/WKL.glob theories/Logic/WeakFan.glob theories/MSets/MSetAVL.glob theories/MSets/MSetDecide.glob theories/MSets/MSetEqProperties.glob theories/MSets/MSetFacts.glob theories/MSets/MSetGenTree.glob theories/MSets/MSetInterface.glob theories/MSets/MSetList.glob theories/MSets/MSetPositive.glob theories/MSets/MSetProperties.glob theories/MSets/MSetRBT.glob theories/MSets/MSetToFiniteSet.glob theories/MSets/MSetWeakList.glob theories/MSets/MSets.glob theories/NArith/BinNat.glob theories/NArith/BinNatDef.glob theories/NArith/NArith.glob theories/NArith/Ndec.glob theories/NArith/Ndigits.glob theories/NArith/Ndist.glob theories/NArith/Ndiv_def.glob theories/NArith/Ngcd_def.glob theories/NArith/Nnat.glob theories/NArith/Nsqrt_def.glob theories/Numbers/AltBinNotations.glob theories/Numbers/BinNums.glob theories/Numbers/Cyclic/Abstract/CyclicAxioms.glob theories/Numbers/Cyclic/Abstract/DoubleType.glob theories/Numbers/Cyclic/Abstract/NZCyclic.glob theories/Numbers/Cyclic/Int31/Cyclic31.glob theories/Numbers/Cyclic/Int31/Int31.glob theories/Numbers/Cyclic/Int31/Ring31.glob theories/Numbers/Cyclic/Int63/Cyclic63.glob theories/Numbers/Cyclic/Int63/Int63.glob theories/Numbers/Cyclic/Int63/Ring63.glob theories/Numbers/Cyclic/ZModulo/ZModulo.glob theories/Numbers/DecimalFacts.glob theories/Numbers/DecimalN.glob theories/Numbers/DecimalNat.glob theories/Numbers/DecimalPos.glob theories/Numbers/DecimalQ.glob theories/Numbers/DecimalString.glob theories/Numbers/DecimalZ.glob theories/Numbers/HexadecimalFacts.glob theories/Numbers/HexadecimalN.glob theories/Numbers/HexadecimalNat.glob theories/Numbers/HexadecimalPos.glob theories/Numbers/HexadecimalQ.glob theories/Numbers/HexadecimalString.glob theories/Numbers/HexadecimalZ.glob theories/Numbers/Integer/Abstract/ZAdd.glob theories/Numbers/Integer/Abstract/ZAddOrder.glob theories/Numbers/Integer/Abstract/ZAxioms.glob theories/Numbers/Integer/Abstract/ZBase.glob theories/Numbers/Integer/Abstract/ZBits.glob theories/Numbers/Integer/Abstract/ZDivEucl.glob theories/Numbers/Integer/Abstract/ZDivFloor.glob theories/Numbers/Integer/Abstract/ZDivTrunc.glob theories/Numbers/Integer/Abstract/ZGcd.glob theories/Numbers/Integer/Abstract/ZLcm.glob theories/Numbers/Integer/Abstract/ZLt.glob theories/Numbers/Integer/Abstract/ZMaxMin.glob theories/Numbers/Integer/Abstract/ZMul.glob theories/Numbers/Integer/Abstract/ZMulOrder.glob theories/Numbers/Integer/Abstract/ZParity.glob theories/Numbers/Integer/Abstract/ZPow.glob theories/Numbers/Integer/Abstract/ZProperties.glob theories/Numbers/Integer/Abstract/ZSgnAbs.glob theories/Numbers/Integer/Binary/ZBinary.glob theories/Numbers/Integer/NatPairs/ZNatPairs.glob theories/Numbers/NaryFunctions.glob theories/Numbers/NatInt/NZAdd.glob theories/Numbers/NatInt/NZAddOrder.glob theories/Numbers/NatInt/NZAxioms.glob theories/Numbers/NatInt/NZBase.glob theories/Numbers/NatInt/NZBits.glob theories/Numbers/NatInt/NZDiv.glob theories/Numbers/NatInt/NZDomain.glob theories/Numbers/NatInt/NZGcd.glob theories/Numbers/NatInt/NZLog.glob theories/Numbers/NatInt/NZMul.glob theories/Numbers/NatInt/NZMulOrder.glob theories/Numbers/NatInt/NZOrder.glob theories/Numbers/NatInt/NZParity.glob theories/Numbers/NatInt/NZPow.glob theories/Numbers/NatInt/NZProperties.glob theories/Numbers/NatInt/NZSqrt.glob theories/Numbers/Natural/Abstract/NAdd.glob theories/Numbers/Natural/Abstract/NAddOrder.glob theories/Numbers/Natural/Abstract/NAxioms.glob theories/Numbers/Natural/Abstract/NBase.glob theories/Numbers/Natural/Abstract/NBits.glob theories/Numbers/Natural/Abstract/NDefOps.glob theories/Numbers/Natural/Abstract/NDiv.glob theories/Numbers/Natural/Abstract/NGcd.glob theories/Numbers/Natural/Abstract/NIso.glob theories/Numbers/Natural/Abstract/NLcm.glob theories/Numbers/Natural/Abstract/NLog.glob theories/Numbers/Natural/Abstract/NMaxMin.glob theories/Numbers/Natural/Abstract/NMulOrder.glob theories/Numbers/Natural/Abstract/NOrder.glob theories/Numbers/Natural/Abstract/NParity.glob theories/Numbers/Natural/Abstract/NPow.glob theories/Numbers/Natural/Abstract/NProperties.glob theories/Numbers/Natural/Abstract/NSqrt.glob theories/Numbers/Natural/Abstract/NStrongRec.glob theories/Numbers/Natural/Abstract/NSub.glob theories/Numbers/Natural/Binary/NBinary.glob theories/Numbers/Natural/Peano/NPeano.glob theories/Numbers/NumPrelude.glob theories/PArith/BinPos.glob theories/PArith/BinPosDef.glob theories/PArith/PArith.glob theories/PArith/POrderedType.glob theories/PArith/Pnat.glob theories/Program/Basics.glob theories/Program/Combinators.glob theories/Program/Equality.glob theories/Program/Program.glob theories/Program/Subset.glob theories/Program/Syntax.glob theories/Program/Tactics.glob theories/Program/Utils.glob theories/Program/Wf.glob theories/QArith/QArith.glob theories/QArith/QArith_base.glob theories/QArith/QOrderedType.glob theories/QArith/Qabs.glob theories/QArith/Qcabs.glob theories/QArith/Qcanon.glob theories/QArith/Qfield.glob theories/QArith/Qminmax.glob theories/QArith/Qpower.glob theories/QArith/Qreals.glob theories/QArith/Qreduction.glob theories/QArith/Qring.glob theories/QArith/Qround.glob theories/Reals/Abstract/ConstructiveAbs.glob theories/Reals/Abstract/ConstructiveLUB.glob theories/Reals/Abstract/ConstructiveLimits.glob theories/Reals/Abstract/ConstructiveMinMax.glob theories/Reals/Abstract/ConstructivePower.glob theories/Reals/Abstract/ConstructiveReals.glob theories/Reals/Abstract/ConstructiveRealsMorphisms.glob theories/Reals/Abstract/ConstructiveSum.glob theories/Reals/Alembert.glob theories/Reals/AltSeries.glob theories/Reals/ArithProp.glob theories/Reals/Binomial.glob theories/Reals/Cauchy/ConstructiveCauchyAbs.glob theories/Reals/Cauchy/ConstructiveCauchyReals.glob theories/Reals/Cauchy/ConstructiveCauchyRealsMult.glob theories/Reals/Cauchy/ConstructiveRcomplete.glob theories/Reals/Cauchy_prod.glob theories/Reals/ClassicalConstructiveReals.glob theories/Reals/ClassicalDedekindReals.glob theories/Reals/Cos_plus.glob theories/Reals/Cos_rel.glob theories/Reals/DiscrR.glob theories/Reals/Exp_prop.glob theories/Reals/Integration.glob theories/Reals/MVT.glob theories/Reals/Machin.glob theories/Reals/NewtonInt.glob theories/Reals/PSeries_reg.glob theories/Reals/PartSum.glob theories/Reals/RIneq.glob theories/Reals/RList.glob theories/Reals/ROrderedType.glob theories/Reals/R_Ifp.glob theories/Reals/R_sqr.glob theories/Reals/R_sqrt.glob theories/Reals/Ranalysis.glob theories/Reals/Ranalysis1.glob theories/Reals/Ranalysis2.glob theories/Reals/Ranalysis3.glob theories/Reals/Ranalysis4.glob theories/Reals/Ranalysis5.glob theories/Reals/Ranalysis_reg.glob theories/Reals/Ratan.glob theories/Reals/Raxioms.glob theories/Reals/Rbase.glob theories/Reals/Rbasic_fun.glob theories/Reals/Rcomplete.glob theories/Reals/Rdefinitions.glob theories/Reals/Rderiv.glob theories/Reals/Reals.glob theories/Reals/Rfunctions.glob theories/Reals/Rgeom.glob theories/Reals/RiemannInt.glob theories/Reals/RiemannInt_SF.glob theories/Reals/Rlimit.glob theories/Reals/Rlogic.glob theories/Reals/Rminmax.glob theories/Reals/Rpow_def.glob theories/Reals/Rpower.glob theories/Reals/Rprod.glob theories/Reals/Rregisternames.glob theories/Reals/Rseries.glob theories/Reals/Rsigma.glob theories/Reals/Rsqrt_def.glob theories/Reals/Rtopology.glob theories/Reals/Rtrigo.glob theories/Reals/Rtrigo1.glob theories/Reals/Rtrigo_alt.glob theories/Reals/Rtrigo_calc.glob theories/Reals/Rtrigo_def.glob theories/Reals/Rtrigo_facts.glob theories/Reals/Rtrigo_fun.glob theories/Reals/Rtrigo_reg.glob theories/Reals/Runcountable.glob theories/Reals/SeqProp.glob theories/Reals/SeqSeries.glob theories/Reals/SplitAbsolu.glob theories/Reals/SplitRmult.glob theories/Reals/Sqrt_reg.glob theories/Relations/Operators_Properties.glob theories/Relations/Relation_Definitions.glob theories/Relations/Relation_Operators.glob theories/Relations/Relations.glob theories/Setoids/Setoid.glob theories/Sets/Classical_sets.glob theories/Sets/Constructive_sets.glob theories/Sets/Cpo.glob theories/Sets/Ensembles.glob theories/Sets/Finite_sets.glob theories/Sets/Finite_sets_facts.glob theories/Sets/Image.glob theories/Sets/Infinite_sets.glob theories/Sets/Integers.glob theories/Sets/Multiset.glob theories/Sets/Partial_Order.glob theories/Sets/Permut.glob theories/Sets/Powerset.glob theories/Sets/Powerset_Classical_facts.glob theories/Sets/Powerset_facts.glob theories/Sets/Relations_1.glob theories/Sets/Relations_1_facts.glob theories/Sets/Relations_2.glob theories/Sets/Relations_2_facts.glob theories/Sets/Relations_3.glob theories/Sets/Relations_3_facts.glob theories/Sets/Uniset.glob theories/Sorting/CPermutation.glob theories/Sorting/Heap.glob theories/Sorting/Mergesort.glob theories/Sorting/PermutEq.glob theories/Sorting/PermutSetoid.glob theories/Sorting/Permutation.glob theories/Sorting/Sorted.glob theories/Sorting/Sorting.glob theories/Strings/Ascii.glob theories/Strings/BinaryString.glob theories/Strings/Byte.glob theories/Strings/ByteVector.glob theories/Strings/HexString.glob theories/Strings/OctalString.glob theories/Strings/String.glob theories/Structures/DecidableType.glob theories/Structures/DecidableTypeEx.glob theories/Structures/Equalities.glob theories/Structures/EqualitiesFacts.glob theories/Structures/GenericMinMax.glob theories/Structures/OrderedType.glob theories/Structures/OrderedTypeAlt.glob theories/Structures/OrderedTypeEx.glob theories/Structures/Orders.glob theories/Structures/OrdersAlt.glob theories/Structures/OrdersEx.glob theories/Structures/OrdersFacts.glob theories/Structures/OrdersLists.glob theories/Structures/OrdersTac.glob theories/Unicode/Utf8.glob theories/Unicode/Utf8_core.glob theories/Vectors/Fin.glob theories/Vectors/Vector.glob theories/Vectors/VectorDef.glob theories/Vectors/VectorEq.glob theories/Vectors/VectorSpec.glob theories/Wellfounded/Disjoint_Union.glob theories/Wellfounded/Inclusion.glob theories/Wellfounded/Inverse_Image.glob theories/Wellfounded/Lexicographic_Exponentiation.glob theories/Wellfounded/Lexicographic_Product.glob theories/Wellfounded/Transitive_Closure.glob theories/Wellfounded/Union.glob theories/Wellfounded/Well_Ordering.glob theories/Wellfounded/Wellfounded.glob theories/ZArith/BinInt.glob theories/ZArith/BinIntDef.glob theories/ZArith/Int.glob theories/ZArith/Wf_Z.glob theories/ZArith/ZArith.glob theories/ZArith/ZArith_base.glob theories/ZArith/ZArith_dec.glob theories/ZArith/Zabs.glob theories/ZArith/Zbool.glob theories/ZArith/Zcompare.glob theories/ZArith/Zcomplements.glob theories/ZArith/Zdigits.glob theories/ZArith/Zdiv.glob theories/ZArith/Zeuclid.glob theories/ZArith/Zeven.glob theories/ZArith/Zgcd_alt.glob theories/ZArith/Zhints.glob theories/ZArith/Zmax.glob theories/ZArith/Zmin.glob theories/ZArith/Zminmax.glob theories/ZArith/Zmisc.glob theories/ZArith/Znat.glob theories/ZArith/Znumtheory.glob theories/ZArith/Zorder.glob theories/ZArith/Zpow_alt.glob theories/ZArith/Zpow_def.glob theories/ZArith/Zpow_facts.glob theories/ZArith/Zpower.glob theories/ZArith/Zquot.glob theories/ZArith/Zwf.glob theories/ZArith/auxiliary.glob theories/btauto/Algebra.glob theories/btauto/Btauto.glob theories/btauto/Reflect.glob theories/derive/Derive.glob theories/ssr/ssrbool.glob theories/ssr/ssrclasses.glob theories/ssr/ssreflect.glob theories/ssr/ssrfun.glob theories/ssr/ssrsetoid.glob theories/ssr/ssrunder.glob theories/extraction/ExtrHaskellBasic.glob theories/extraction/ExtrHaskellNatInt.glob theories/extraction/ExtrHaskellNatInteger.glob theories/extraction/ExtrHaskellNatNum.glob theories/extraction/ExtrHaskellString.glob theories/extraction/ExtrHaskellZInt.glob theories/extraction/ExtrHaskellZInteger.glob theories/extraction/ExtrHaskellZNum.glob theories/extraction/ExtrOCamlFloats.glob theories/extraction/ExtrOCamlInt63.glob theories/extraction/ExtrOcamlBasic.glob theories/extraction/ExtrOcamlBigIntConv.glob theories/extraction/ExtrOcamlChar.glob theories/extraction/ExtrOcamlIntConv.glob theories/extraction/ExtrOcamlNatBigInt.glob theories/extraction/ExtrOcamlNatInt.glob theories/extraction/ExtrOcamlString.glob theories/extraction/ExtrOcamlNativeString.glob theories/extraction/ExtrOcamlZBigInt.glob theories/extraction/ExtrOcamlZInt.glob theories/extraction/Extraction.glob theories/funind/FunInd.glob theories/funind/Recdef.glob theories/micromega/DeclConstant.glob theories/micromega/Env.glob theories/micromega/EnvRing.glob theories/micromega/Fourier.glob theories/micromega/Fourier_util.glob theories/micromega/Lia.glob theories/micromega/Lqa.glob theories/micromega/Lra.glob theories/micromega/MExtraction.glob theories/micromega/OrderedRing.glob theories/micromega/Psatz.glob theories/micromega/QMicromega.glob theories/micromega/RMicromega.glob theories/micromega/Refl.glob theories/micromega/RingMicromega.glob theories/micromega/Tauto.glob theories/micromega/VarMap.glob theories/micromega/ZArith_hints.glob theories/micromega/ZCoeff.glob theories/micromega/ZMicromega.glob theories/micromega/Zify.glob theories/micromega/ZifyBool.glob theories/micromega/ZifyClasses.glob theories/micromega/ZifyInst.glob theories/micromega/ZifyComparison.glob theories/micromega/ZifyPow.glob theories/micromega/Ztac.glob theories/nsatz/Nsatz.glob theories/nsatz/NsatzTactic.glob theories/omega/Omega.glob theories/omega/OmegaLemmas.glob theories/omega/OmegaPlugin.glob theories/omega/OmegaTactic.glob theories/omega/PreOmega.glob theories/rtauto/Bintree.glob theories/rtauto/Rtauto.glob theories/setoid_ring/Algebra_syntax.glob theories/setoid_ring/ArithRing.glob theories/setoid_ring/BinList.glob theories/setoid_ring/Cring.glob theories/setoid_ring/Field.glob theories/setoid_ring/Field_tac.glob theories/setoid_ring/Field_theory.glob theories/setoid_ring/InitialRing.glob theories/setoid_ring/Integral_domain.glob theories/setoid_ring/NArithRing.glob theories/setoid_ring/Ncring.glob theories/setoid_ring/Ncring_initial.glob theories/setoid_ring/Ncring_polynom.glob theories/setoid_ring/Ncring_tac.glob theories/setoid_ring/RealField.glob theories/setoid_ring/Ring.glob theories/setoid_ring/Ring_base.glob theories/setoid_ring/Ring_polynom.glob theories/setoid_ring/Ring_tac.glob theories/setoid_ring/Ring_theory.glob theories/setoid_ring/Rings_Q.glob theories/setoid_ring/Rings_R.glob theories/setoid_ring/Rings_Z.glob theories/setoid_ring/ZArithRing.glob theories/ssrmatching/ssrmatching.glob theories/ssrsearch/ssrsearch.glob usercontrib/Ltac2/Array.glob usercontrib/Ltac2/Bool.glob usercontrib/Ltac2/Char.glob usercontrib/Ltac2/Constr.glob usercontrib/Ltac2/Control.glob usercontrib/Ltac2/Env.glob usercontrib/Ltac2/Fresh.glob usercontrib/Ltac2/Ident.glob usercontrib/Ltac2/Init.glob usercontrib/Ltac2/Int.glob usercontrib/Ltac2/List.glob usercontrib/Ltac2/Ltac1.glob usercontrib/Ltac2/Ltac2.glob usercontrib/Ltac2/Message.glob usercontrib/Ltac2/Notations.glob usercontrib/Ltac2/Option.glob usercontrib/Ltac2/Pattern.glob usercontrib/Ltac2/Std.glob usercontrib/Ltac2/String.glob
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/usercontrib
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/kernel/byterun
install m 644 kernel/byterun/dllcoqrun.so "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/kernel/byterun
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/plugins/micromega
install plugins/micromega/csdpcert "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/plugins/micromega
rm f "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/revision
install m 644 revision "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
install: revision: No such file or directory
gmake[1]: [Makefile.install:134: installlibrary] Error 1 (ignored)
Makefile.install:154: warning: undefined variable 'OLDROOT'
Makefile.install:155: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/man"/man1
install m 644 man/coqtex.1 man/coqdep.1 man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 man/coqwc.1 man/coqdoc.1 man/coqide.1 man/coq_makefile.1 man/coqchk.1 "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/man"/man1
Makefile.install:161: warning: undefined variable 'OLDROOT'
Makefile.install:162: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/texmf/tex/latex/misc"
install m 644 tools/coqdoc/coqdoc.sty "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/texmf/tex/latex/misc"
Makefile.install:104: warning: undefined variable 'OLDROOT'
Makefile.install:105: warning: undefined variable 'OLDROOT'
Makefile.install:106: warning: undefined variable 'OLDROOT'
Makefile.install:107: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" clib/bigint.cmi clib/cArray.cmi clib/cEphemeron.cmi clib/cList.cmi clib/cMap.cmi clib/cObj.cmi clib/cSet.cmi clib/cSig.cmi clib/cString.cmi clib/cThread.cmi clib/cUnix.cmi clib/diff2.cmi clib/dyn.cmi clib/exninfo.cmi clib/hMap.cmi clib/hashcons.cmi clib/hashset.cmi clib/heap.cmi clib/iStream.cmi clib/int.cmi clib/minisys.cmi clib/monad.cmi clib/option.cmi clib/orderedType.cmi clib/predicate.cmi clib/range.cmi clib/segmenttree.cmi clib/store.cmi clib/terminal.cmi clib/trie.cmi clib/unicode.cmi clib/unicodetable.cmi clib/unionfind.cmi config/coq_config.cmi coqpp/coqpp_ast.cmi coqpp/coqpp_parse.cmi coqpp/coqpp_parser.cmi dev/top_printers.cmi engine/eConstr.cmi engine/evar_kinds.cmi engine/evarutil.cmi engine/evd.cmi engine/ftactic.cmi engine/logic_monad.cmi engine/namegen.cmi engine/nameops.cmi engine/proofview.cmi engine/proofview_monad.cmi engine/termops.cmi engine/uState.cmi engine/univGen.cmi engine/univMinim.cmi engine/univNames.cmi engine/univProblem.cmi engine/univSubst.cmi engine/univops.cmi gramlib/.pack/gramlib.cmi gramlib/.pack/gramlib__Gramext.cmi gramlib/.pack/gramlib__Grammar.cmi gramlib/.pack/gramlib__Plexing.cmi gramlib/.pack/gramlib__Ploc.cmi interp/constrexpr.cmi interp/constrexpr_ops.cmi interp/constrextern.cmi interp/constrintern.cmi interp/decls.cmi interp/deprecation.cmi interp/dumpglob.cmi interp/genintern.cmi interp/impargs.cmi interp/implicit_quantifiers.cmi interp/modintern.cmi interp/notation.cmi interp/notation_ops.cmi interp/notation_term.cmi interp/numTok.cmi interp/reserve.cmi interp/smartlocate.cmi interp/stdarg.cmi interp/syntax_def.cmi kernel/cClosure.cmi kernel/cPrimitives.cmi kernel/cbytecodes.cmi kernel/cbytegen.cmi kernel/cemitcodes.cmi kernel/clambda.cmi kernel/constr.cmi kernel/context.cmi kernel/conv_oracle.cmi kernel/cooking.cmi kernel/copcodes.cmi kernel/csymtable.cmi kernel/declarations.cmi kernel/declareops.cmi kernel/entries.cmi kernel/environ.cmi kernel/esubst.cmi kernel/evar.cmi kernel/float64.cmi kernel/indTyping.cmi kernel/indtypes.cmi kernel/inductive.cmi kernel/inferCumulativity.cmi kernel/mod_subst.cmi kernel/mod_typing.cmi kernel/modops.cmi kernel/names.cmi kernel/nativecode.cmi kernel/nativeconv.cmi kernel/nativelambda.cmi kernel/nativelib.cmi kernel/nativelibrary.cmi kernel/nativevalues.cmi kernel/opaqueproof.cmi kernel/primred.cmi kernel/reduction.cmi kernel/relevanceops.cmi kernel/retroknowledge.cmi kernel/safe_typing.cmi kernel/section.cmi kernel/sorts.cmi kernel/subtyping.cmi kernel/term.cmi kernel/term_typing.cmi kernel/transparentState.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/uGraph.cmi kernel/uint63.cmi kernel/univ.cmi kernel/vars.cmi kernel/vconv.cmi kernel/vm.cmi kernel/vmvalues.cmi lib/acyclicGraph.cmi lib/aux_file.cmi lib/cAst.cmi lib/cErrors.cmi lib/cProfile.cmi lib/cWarnings.cmi lib/control.cmi lib/coqProject_file.cmi lib/dAst.cmi lib/envars.cmi lib/explore.cmi lib/feedback.cmi lib/flags.cmi lib/future.cmi lib/genarg.cmi lib/hook.cmi lib/loc.cmi lib/objFile.cmi lib/pp.cmi lib/pp_diff.cmi lib/remoteCounter.cmi lib/rtree.cmi lib/spawn.cmi lib/stateid.cmi lib/system.cmi lib/util.cmi lib/xml_datatype.cmi library/coqlib.cmi library/global.cmi library/globnames.cmi library/goptions.cmi library/lib.cmi library/libnames.cmi library/libobject.cmi library/nametab.cmi library/states.cmi library/summary.cmi parsing/cLexer.cmi parsing/extend.cmi parsing/g_constr.cmi parsing/g_prim.cmi parsing/notation_gram.cmi parsing/notgram_ops.cmi parsing/pcoq.cmi parsing/ppextend.cmi parsing/tok.cmi plugins/btauto/refl_btauto.cmi plugins/cc/ccalgo.cmi plugins/cc/ccproof.cmi plugins/cc/cctac.cmi plugins/derive/derive.cmi plugins/extraction/common.cmi plugins/extraction/extract_env.cmi plugins/extraction/extraction.cmi plugins/extraction/haskell.cmi plugins/extraction/json.cmi plugins/extraction/miniml.cmi plugins/extraction/mlutil.cmi plugins/extraction/modutil.cmi plugins/extraction/ocaml.cmi plugins/extraction/scheme.cmi plugins/extraction/table.cmi plugins/firstorder/formula.cmi plugins/firstorder/ground.cmi plugins/firstorder/instances.cmi plugins/firstorder/rules.cmi plugins/firstorder/sequent.cmi plugins/firstorder/unify.cmi plugins/funind/functional_principles_proofs.cmi plugins/funind/functional_principles_types.cmi plugins/funind/gen_principle.cmi plugins/funind/glob_term_to_relation.cmi plugins/funind/glob_termops.cmi plugins/funind/indfun.cmi plugins/funind/indfun_common.cmi plugins/funind/invfun.cmi plugins/funind/recdef.cmi plugins/ltac/evar_tactics.cmi plugins/ltac/extraargs.cmi plugins/ltac/extratactics.cmi plugins/ltac/leminv.cmi plugins/ltac/pltac.cmi plugins/ltac/pptactic.cmi plugins/ltac/profile_ltac.cmi plugins/ltac/rewrite.cmi plugins/ltac/tacarg.cmi plugins/ltac/taccoerce.cmi plugins/ltac/tacentries.cmi plugins/ltac/tacenv.cmi plugins/ltac/tacexpr.cmi plugins/ltac/tacintern.cmi plugins/ltac/tacinterp.cmi plugins/ltac/tacsubst.cmi plugins/ltac/tactic_debug.cmi plugins/ltac/tactic_matching.cmi plugins/ltac/tactic_option.cmi plugins/ltac/tauto.cmi plugins/micromega/certificate.cmi plugins/micromega/coq_micromega.cmi plugins/micromega/csdpcert.cmi plugins/micromega/g_micromega.cmi plugins/micromega/itv.cmi plugins/micromega/mfourier.cmi plugins/micromega/micromega.cmi plugins/micromega/mutils.cmi plugins/micromega/numCompat.cmi plugins/micromega/persistent_cache.cmi plugins/micromega/polynomial.cmi plugins/micromega/simplex.cmi plugins/micromega/sos.cmi plugins/micromega/sos_lib.cmi plugins/micromega/sos_types.cmi plugins/micromega/vect.cmi plugins/micromega/zify.cmi plugins/nsatz/ideal.cmi plugins/nsatz/nsatz.cmi plugins/nsatz/polynom.cmi plugins/nsatz/utile.cmi plugins/omega/coq_omega.cmi plugins/rtauto/proof_search.cmi plugins/rtauto/refl_tauto.cmi plugins/setoid_ring/newring.cmi plugins/setoid_ring/newring_ast.cmi plugins/ssr/ssrast.cmi plugins/ssr/ssrbwd.cmi plugins/ssr/ssrcommon.cmi plugins/ssr/ssrelim.cmi plugins/ssr/ssrequality.cmi plugins/ssr/ssrfwd.cmi plugins/ssr/ssripats.cmi plugins/ssr/ssrparser.cmi plugins/ssr/ssrprinters.cmi plugins/ssr/ssrtacticals.cmi plugins/ssr/ssrvernac.cmi plugins/ssr/ssrview.cmi plugins/ssrmatching/g_ssrmatching.cmi plugins/ssrmatching/ssrmatching.cmi plugins/syntax/numeral.cmi plugins/syntax/r_syntax.cmi plugins/syntax/string_notation.cmi pretyping/arguments_renaming.cmi pretyping/cases.cmi pretyping/cbv.cmi pretyping/coercion.cmi pretyping/coercionops.cmi pretyping/constr_matching.cmi pretyping/detyping.cmi pretyping/evarconv.cmi pretyping/evardefine.cmi pretyping/evarsolve.cmi pretyping/find_subterm.cmi pretyping/geninterp.cmi pretyping/globEnv.cmi pretyping/glob_ops.cmi pretyping/glob_term.cmi pretyping/heads.cmi pretyping/indrec.cmi pretyping/inductiveops.cmi pretyping/keys.cmi pretyping/locus.cmi pretyping/locusops.cmi pretyping/ltac_pretype.cmi pretyping/nativenorm.cmi pretyping/pattern.cmi pretyping/patternops.cmi pretyping/pretype_errors.cmi pretyping/pretyping.cmi pretyping/program.cmi pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi pretyping/tacred.cmi pretyping/typeclasses.cmi pretyping/typeclasses_errors.cmi pretyping/typing.cmi pretyping/unification.cmi pretyping/vnorm.cmi printing/genprint.cmi printing/ppconstr.cmi printing/pputils.cmi printing/printer.cmi printing/printmod.cmi printing/proof_diffs.cmi proofs/clenv.cmi proofs/clenvtac.cmi proofs/evar_refiner.cmi proofs/goal.cmi proofs/goal_select.cmi proofs/logic.cmi proofs/miscprint.cmi proofs/proof.cmi proofs/proof_bullet.cmi proofs/refine.cmi proofs/refiner.cmi proofs/tacmach.cmi proofs/tactypes.cmi stm/asyncTaskQueue.cmi stm/coqworkmgrApi.cmi stm/dag.cmi stm/proofBlockDelimiter.cmi stm/spawned.cmi stm/stm.cmi stm/tQueue.cmi stm/vcs.cmi stm/vernac_classifier.cmi stm/vio_checking.cmi stm/workerPool.cmi tactics/abstract.cmi tactics/auto.cmi tactics/autorewrite.cmi tactics/btermdn.cmi tactics/class_tactics.cmi tactics/contradiction.cmi tactics/declareScheme.cmi tactics/declareUctx.cmi tactics/dn.cmi tactics/dnet.cmi tactics/eauto.cmi tactics/elim.cmi tactics/elimschemes.cmi tactics/eqdecide.cmi tactics/eqschemes.cmi tactics/equality.cmi tactics/genredexpr.cmi tactics/hints.cmi tactics/hipattern.cmi tactics/ind_tables.cmi tactics/inv.cmi tactics/ppred.cmi tactics/redexpr.cmi tactics/redops.cmi tactics/tacticals.cmi tactics/tactics.cmi tactics/term_dnet.cmi toplevel/ccompile.cmi toplevel/coqargs.cmi toplevel/coqc.cmi toplevel/coqcargs.cmi toplevel/coqinit.cmi toplevel/coqloop.cmi toplevel/coqtop.cmi toplevel/g_toplevel.cmi toplevel/usage.cmi toplevel/vernac.cmi toplevel/workerLoop.cmi usercontrib/Ltac2/tac2core.cmi usercontrib/Ltac2/tac2dyn.cmi usercontrib/Ltac2/tac2entries.cmi usercontrib/Ltac2/tac2env.cmi usercontrib/Ltac2/tac2expr.cmi usercontrib/Ltac2/tac2extffi.cmi usercontrib/Ltac2/tac2ffi.cmi usercontrib/Ltac2/tac2intern.cmi usercontrib/Ltac2/tac2interp.cmi usercontrib/Ltac2/tac2match.cmi usercontrib/Ltac2/tac2print.cmi usercontrib/Ltac2/tac2qexpr.cmi usercontrib/Ltac2/tac2quote.cmi usercontrib/Ltac2/tac2stdlib.cmi usercontrib/Ltac2/tac2tactics.cmi usercontrib/Ltac2/tac2types.cmi vernac/assumptions.cmi vernac/attributes.cmi vernac/auto_ind_decl.cmi vernac/canonical.cmi vernac/classes.cmi vernac/comArguments.cmi vernac/comAssumption.cmi vernac/comCoercion.cmi vernac/comDefinition.cmi vernac/comFixpoint.cmi vernac/comHints.cmi vernac/comInductive.cmi vernac/comPrimitive.cmi vernac/comProgramFixpoint.cmi vernac/comSearch.cmi vernac/declare.cmi vernac/declareDef.cmi vernac/declareInd.cmi vernac/declareObl.cmi vernac/declareUniv.cmi vernac/declaremods.cmi vernac/egramcoq.cmi vernac/egramml.cmi vernac/g_proofs.cmi vernac/g_vernac.cmi vernac/himsg.cmi vernac/indschemes.cmi vernac/lemmas.cmi vernac/library.cmi vernac/loadpath.cmi vernac/locality.cmi vernac/metasyntax.cmi vernac/mltop.cmi vernac/obligations.cmi vernac/pfedit.cmi vernac/ppvernac.cmi vernac/prettyp.cmi vernac/proof_global.cmi vernac/proof_using.cmi vernac/pvernac.cmi vernac/recLemmas.cmi vernac/record.cmi vernac/retrieveObl.cmi vernac/search.cmi vernac/topfmt.cmi vernac/vernacentries.cmi vernac/vernacexpr.cmi vernac/vernacextend.cmi vernac/vernacinterp.cmi vernac/vernacprop.cmi vernac/vernacstate.cmi plugins/ltac/ltac_plugin.cmi plugins/ltac/tauto_plugin.cmi plugins/omega/omega_plugin.cmi plugins/micromega/micromega_plugin.cmi plugins/setoid_ring/newring_plugin.cmi plugins/extraction/extraction_plugin.cmi plugins/cc/cc_plugin.cmi plugins/firstorder/ground_plugin.cmi plugins/rtauto/rtauto_plugin.cmi plugins/btauto/btauto_plugin.cmi plugins/funind/recdef_plugin.cmi plugins/nsatz/nsatz_plugin.cmi plugins/syntax/r_syntax_plugin.cmi plugins/syntax/int63_syntax_plugin.cmi plugins/syntax/float_syntax_plugin.cmi plugins/syntax/numeral_notation_plugin.cmi plugins/syntax/string_notation_plugin.cmi plugins/derive/derive_plugin.cmi plugins/ssrmatching/ssrmatching_plugin.cmi plugins/ssr/ssreflect_plugin.cmi plugins/ssrsearch/ssrsearch_plugin.cmi usercontrib/Ltac2/ltac2_plugin.cmi plugins/micromega/zify_plugin.cmi # Regular CMI files
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" tools/CoqMakefile.in tools/makeonetimefile.py tools/TimeFileMaker.py tools/makebothtimefiles.py tools/makebothsingletimingfiles.py
Makefile.ide:196: warning: undefined variable 'OLDROOT'
Makefile.ide:197: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" ide/ide.cma
Makefile.ide:200: warning: undefined variable 'OLDROOT'
Makefile.ide:201: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
install bin/coqide "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
Makefile.ide:209: warning: undefined variable 'OLDROOT'
install bin/coqidetop bin/coqidetop.byte "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
Makefile.ide:221: warning: undefined variable 'OLDROOT'
Makefile.ide:222: warning: undefined variable 'OLDROOT'
Makefile.ide:223: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/coq"
install m 644 ide/coq.png ide/*.lang ide/coq_style.xml ide/default.bindings "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/coq"
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/etc/xdg/coq"
Makefile.ide:226: warning: undefined variable 'OLDROOT'
Makefile.ide:227: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/doc/coq"
install m 644 ide/FAQ "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/doc/coq"/FAQCoqIde
Makefile.ide:213: warning: undefined variable 'OLDROOT'
Makefile.ide:214: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" \
ide/minilib.cmi ide/configwin_messages.cmi ide/configwin_ihm.cmi ide/configwin.cmi ide/tags.cmi ide/wg_Notebook.cmi ide/config_lexer.cmi ide/utf8_convert.cmi ide/preferences.cmi ide/ideutils.cmi ide/unicode_bindings.cmi ide/coq.cmi ide/coq_lex.cmi ide/sentence.cmi ide/gtk_parsing.cmi ide/wg_Segment.cmi ide/wg_ProofView.cmi ide/wg_MessageView.cmi ide/wg_RoutedMessageViews.cmi ide/wg_Detachable.cmi ide/wg_Find.cmi ide/wg_Completion.cmi ide/wg_ScriptView.cmi ide/coq_commands.cmi ide/fileOps.cmi ide/document.cmi ide/coqOps.cmi ide/wg_Command.cmi ide/session.cmi ide/coqide_ui.cmi ide/microPG.cmi ide/coqide.cmi
Makefile.install:74: warning: undefined variable 'OLDROOT'
Makefile.install:75: warning: undefined variable 'OLDROOT'
Makefile.install:76: warning: undefined variable 'OLDROOT'
Makefile.install:77: warning: undefined variable 'OLDROOT'
install d "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
install bin/coqtop.byte bin/coqproofworker.byte bin/coqtacticworker.byte bin/coqqueryworker.byte "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/bin"
./install.sh "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq" config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma gramlib/.pack/gramlib.cma parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma stm/stm.cma toplevel/toplevel.cma plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo plugins/omega/omega_plugin.cmo plugins/micromega/micromega_plugin.cmo plugins/setoid_ring/newring_plugin.cmo plugins/extraction/extraction_plugin.cmo plugins/cc/cc_plugin.cmo plugins/firstorder/ground_plugin.cmo plugins/rtauto/rtauto_plugin.cmo plugins/btauto/btauto_plugin.cmo plugins/funind/recdef_plugin.cmo plugins/nsatz/nsatz_plugin.cmo plugins/syntax/r_syntax_plugin.cmo plugins/syntax/int63_syntax_plugin.cmo plugins/syntax/float_syntax_plugin.cmo plugins/syntax/numeral_notation_plugin.cmo plugins/syntax/string_notation_plugin.cmo plugins/derive/derive_plugin.cmo plugins/ssrmatching/ssrmatching_plugin.cmo plugins/ssr/ssreflect_plugin.cmo plugins/ssrsearch/ssrsearch_plugin.cmo usercontrib/Ltac2/ltac2_plugin.cmo plugins/micromega/zify_plugin.cmo
install m 644 kernel/byterun/dllcoqrun.so "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"
gmake[1]: Nothing to be done for 'installbyte'.
Makefile.install:166: warning: undefined variable 'OLDROOT'
install m 644 META.coq "/usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq"/META
gmake[1]: Leaving directory '/usr/obj/ports/coq8.12.0/coq8.12.0'
gmake: 'installbyte' is up to date.
gmake: 'installmeta' is up to date.
/usr/obj/ports/coq8.12.0/bin/install d m 755 /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/doc/coq/
/usr/obj/ports/coq8.12.0/bin/install c m 644 /usr/obj/ports/coq8.12.0/coq8.12.0/{LICENSE,CREDITS,CONTRIBUTING.md,README.md} /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/share/doc/coq/
>>> Running package in math/coq at 1600015956.93
===> math/coq
`/usr/obj/ports/coq8.12.0/fakeaarch64/.fake_done' is up to date.
===> Building package for coq8.12.0
Create /usr/ports/packages/aarch64/all/coq8.12.0.tgz
Creating package coq8.12.0
reading plist[K[K
switching to /usr/ports/math/coq/pkg/PFRAG.nonative[K[K
[53C[K[K
[53C\[K[K
checking dependencies[K[K
[22Clang/ocaml[K[K
[22Cx11/lablgtk3[K[K
checksumming[K[K
[13C  0%[K
[13C  1%[K
[13C*  1%[K
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/btauto/.coqnative/NCoq_btauto_Algebra.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/btauto/.coqnative/NCoq_btauto_Btauto.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/btauto/.coqnative/NCoq_btauto_Reflect.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/derive/.coqnative/NCoq_derive_Derive.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellBasic.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatInteger.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellNatNum.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellString.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellZInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellZInteger.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrHaskellZNum.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOCamlFloats.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOCamlInt63.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlBasic.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlBigIntConv.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlIntConv.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlNatBigInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlNatInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlString.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlZBigInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_ExtrOcamlZInt.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/extraction/.coqnative/NCoq_extraction_Extraction.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/funind/.coqnative/NCoq_funind_FunInd.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/funind/.coqnative/NCoq_funind_Recdef.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ltac/.coqnative/NCoq_ltac_Ltac.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_DeclConstant.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Env.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_EnvRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Fourier.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Fourier_util.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Lia.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Lqa.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Lra.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_MExtraction.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_OrderedRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Psatz.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_QMicromega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_RMicromega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Refl.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_RingMicromega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Tauto.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_VarMap.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZCoeff.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZMicromega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Zify.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZifyBool.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZifyClasses.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZifyComparison.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZifyInst.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_ZifyPow.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/micromega/.coqnative/NCoq_micromega_Ztac.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/nsatz/.coqnative/NCoq_nsatz_Nsatz.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/omega/.coqnative/NCoq_omega_Omega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/omega/.coqnative/NCoq_omega_OmegaLemmas.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/omega/.coqnative/NCoq_omega_OmegaPlugin.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/omega/.coqnative/NCoq_omega_OmegaTactic.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/omega/.coqnative/NCoq_omega_PreOmega.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/rtauto/.coqnative/NCoq_rtauto_Bintree.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/rtauto/.coqnative/NCoq_rtauto_Rtauto.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Algebra_syntax.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_ArithRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_BinList.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Cring.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Field.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Field_tac.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Field_theory.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_InitialRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Integral_domain.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_NArithRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_initial.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_polynom.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ncring_tac.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_RealField.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ring.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_base.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_polynom.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_tac.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Ring_theory.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_Q.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_R.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_Rings_Z.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/setoid_ring/.coqnative/NCoq_setoid_ring_ZArithRing.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssrbool.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssrclasses.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssreflect.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssrfun.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssrsetoid.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssr/.coqnative/NCoq_ssr_ssrunder.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/plugins/ssrmatching/.coqnative/NCoq_ssrmatching_ssrmatching.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Compat/.coqnative/NCoq_Compat_Coq89.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveCauchyReals.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveCauchyRealsMult.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveRcomplete.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveReals.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveRealsLUB.cmo does not exist
Error: /usr/obj/ports/coq8.12.0/fakeaarch64/usr/local/lib/ocaml/coq/theories/Reals/.coqnative/NCoq_Reals_ConstructiveRealsMorphisms.cmo does not exist
pkg_create: can't continue
*** Error 1 in math/coq (/usr/ports/infrastructure/mk/bsd.port.mk:2124 '/usr/ports/packages/aarch64/all/coq8.12.0.tgz': @trap "cd /usr/port...)
*** Error 2 in math/coq (/usr/ports/infrastructure/mk/bsd.port.mk:2605 '_internalpackage': @case X${_DEPENDS_CACHE} in X) _DEPENDS_CACHE=$...)
*** Error 2 in math/coq (/usr/ports/infrastructure/mk/bsd.port.mk:2584 'package': @lock=coq8.12.0; export _LOCKS_HELD=" coq8.12.0"; /us...)
===> Exiting math/coq with an error
*** Error 1 in /usr/ports (infrastructure/mk/bsd.port.subdir.mk:137 'package': @: ${echo_msg:=echo}; : ${target:=package}; for i in ; do ...)
>>> Running clean in math/coq at 1600015984.39
===> math/coq
===> Cleaning for coq8.12.0
>>> Ended at 1600015987.00
Error: job failed with 512 on localhost at 1600015987