D: [iurt_root_command] chroot
Installing /home/pterjan/rpmbuild/SRPMS/coq-8.5pl2-2.mga7.src.rpm
Executing(%prep): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.VEhtIV
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ cd /home/pterjan/rpmbuild/BUILD
+ rm -rf coq-8.5pl2
+ /usr/bin/gzip -dc /home/pterjan/rpmbuild/SOURCES/coq-8.5pl2.tar.gz
+ /usr/bin/tar -xof -
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd coq-8.5pl2
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ cp /home/pterjan/rpmbuild/SOURCES/Tutorial.pdf /home/pterjan/rpmbuild/SOURCES/Reference-Manual.pdf /home/pterjan/rpmbuild/SOURCES/RecTutorial.pdf .
+ exit 0
Executing(%build): /bin/sh -e /home/pterjan/rpmbuild/tmp/rpm-tmp.58SscE
+ umask 022
+ cd /home/pterjan/rpmbuild/BUILD
+ cd coq-8.5pl2
+ '[' 1 -eq 1 ']'
+ '[' 1 -eq 1 ']'
+ ./configure -mandir /usr/share/man -bindir /usr/bin -libdir /usr/lib64/coq -emacslib /usr/share/emacs/site-lisp -coqdocdir /usr/share/texmf/tex/latex/misc -configdir /etc/xdg/coq -docdir /usr/share/doc/coq -datadir /usr/share/coq -browser 'xdg-open %s' -usecamlp5 -lablgtkdir /usr/lib64/ocaml/lablgtk2 -opt -debug
File "./configure.ml", line 962, characters 45-62:
Warning 3: deprecated: String.capitalize
Use String.capitalize_ascii instead.
File "./configure.ml", line 963, characters 45-62:
Warning 3: deprecated: String.capitalize
Use String.capitalize_ascii instead.
File "./configure.ml", line 964, characters 45-62:
Warning 3: deprecated: String.capitalize
Use String.capitalize_ascii instead.
Warning: obsolete -opt option
You have OCaml 4.06.0. Good!
You have Camlp5 7.03. Good!
You have native-code compilation. Good!
LablGtk2 found (manually provided), with native threads:
=> native CoqIde will be built.

  Architecture                : Linux
  Coq VM bytecode link flags  : -dllib -lcoqrun -dllpath /usr/lib64/coq
  Other bytecode link flags   : 
  OS dependent libraries      : -cclib -lunix
  OCaml version               : 4.06.0
  OCaml binaries in           : /usr/bin
  OCaml library in            : /usr/lib64/ocaml
  Camlp5 version              : 7.03
  Camlp5 binaries in          : /usr/bin
  Camlp5 library in           : +camlp5
  Native dynamic link support : true
  Lablgtk2 library in         : +lablgtk2
  CoqIde                      : opt
  Documentation               : None
  Web browser                 : xdg-open %s
  Coq web site                : http://coq.inria.fr/

  Paths for true installation:
  - the Coq binaries will be copied in /usr/bin
  - the Coq library will be copied in /usr/lib64/coq
  - the Coqide configuration files will be copied in /etc/xdg/coq
  - the Coqide data files will be copied in /usr/share/coq
  - the Coq man pages will be copied in /usr/share/man
  - the Coq documentation will be copied in /usr/share/doc/coq
  - the Coq Emacs mode will be copied in /usr/share/emacs/site-lisp
  - the Coqdoc LaTeX files will be copied in /usr/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'.
+ export CAML_LD_LIBRARY_PATH=/home/pterjan/rpmbuild/BUILD/coq-8.5pl2/kernel/byterun:
+ CAML_LD_LIBRARY_PATH=/home/pterjan/rpmbuild/BUILD/coq-8.5pl2/kernel/byterun:
+ make world
make --warn-undefined-variable --no-builtin-rules -f Makefile.build BUILDGRAMMAR=1 grammar/grammar.cma grammar/q_constr.cmo
make[1]: Entering directory '/home/pterjan/rpmbuild/BUILD/coq-8.5pl2'
OCAMLLEX  tools/coqdep_lexer.mll
406 states, 7873 transitions, table size 33928 bytes
3479 additional bytes used for bindings
OCAMLBEST -o bin/coqdep_boot
File "tools/coqdep_lexer.mll", line 174, characters 22-41:
Warning 3: deprecated: String.uncapitalize
Use String.uncapitalize_ascii instead.
File "tools/coqdep_lexer.mll", line 356, characters 18-37:
Warning 3: deprecated: String.uncapitalize
Use String.uncapitalize_ascii instead.
File "tools/coqdep_lexer.mll", line 361, characters 28-47:
Warning 3: deprecated: String.uncapitalize
Use String.uncapitalize_ascii instead.
OCAMLLEX  ide/config_lexer.mll
30 states, 1657 transitions, table size 6808 bytes
6052 additional bytes used for bindings
OCAMLLEX  ide/coq_lex.mll
30 states, 505 transitions, table size 2200 bytes
OCAMLLEX  ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX  tools/coqwc.mll
230 states, 784 transitions, table size 4516 bytes
OCAMLLEX  tools/coqdoc/cpretty.mll
2652 states, 8247 transitions, table size 48900 bytes
OCAMLLEX  tools/gallina_lexer.mll
190 states, 498 transitions, table size 3132 bytes
OCAMLLEX  lib/xml_lexer.mll
80 states, 774 transitions, table size 3576 bytes
ECHO... > tools/tolink.ml
sed -n -e '/^enum/p' -e 's/,//g' -e '/^  /p' kernel/byterun/coq_instruct.h | \
awk -f kernel/make-opcodes > "kernel/copcodes.ml" || (RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV})
ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml
ECHO... > plugins/derive/derive_plugin_mod.ml
ECHO... > plugins/omega/omega_plugin_mod.ml
ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
ECHO... > plugins/cc/cc_plugin_mod.ml
ECHO... > plugins/fourier/fourier_plugin_mod.ml
ECHO... > plugins/funind/recdef_plugin_mod.ml
ECHO... > plugins/firstorder/ground_plugin_mod.ml
ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
ECHO... > plugins/romega/romega_plugin_mod.ml
ECHO... > plugins/micromega/micromega_plugin_mod.ml
ECHO... > plugins/btauto/btauto_plugin_mod.ml
ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
ECHO... > plugins/extraction/extraction_plugin_mod.ml
ECHO... > plugins/quote/quote_plugin_mod.ml
sed -n -e '/^  /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
               -e '/^}/q' kernel/byterun/coq_instruct.h > "kernel/byterun/coq_jumptbl.h" || (RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV})
"/usr/bin/ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > "theories/Numbers/Natural/BigN/NMake_gen.v" || (RV=$?; rm -f "theories/Numbers/Natural/BigN/NMake_gen.v"; exit ${RV})
COQDEP  grammar/grammar.mllib
*** Warning: inductive.ml already found in kernel (discarding checker/inductive.ml)
*** Warning: safe_typing.mli already found in kernel (discarding checker/safe_typing.mli)
*** Warning: term.ml already found in kernel (discarding checker/term.ml)
*** Warning: subtyping.ml already found in kernel (discarding checker/subtyping.ml)
*** Warning: univ.ml already found in kernel (discarding checker/univ.ml)
*** Warning: environ.ml already found in kernel (discarding checker/environ.ml)
*** Warning: declarations.mli already found in kernel (discarding checker/declarations.mli)
*** Warning: type_errors.ml already found in kernel (discarding checker/type_errors.ml)
*** Warning: type_errors.mli already found in kernel (discarding checker/type_errors.mli)
*** Warning: environ.mli already found in kernel (discarding checker/environ.mli)
*** Warning: subtyping.mli already found in kernel (discarding checker/subtyping.mli)
*** Warning: reduction.mli already found in kernel (discarding checker/reduction.mli)
*** Warning: univ.mli already found in kernel (discarding checker/univ.mli)
*** Warning: closure.mli already found in kernel (discarding checker/closure.mli)
*** Warning: reduction.ml already found in kernel (discarding checker/reduction.ml)
*** Warning: closure.ml already found in kernel (discarding checker/closure.ml)
*** Warning: term.mli already found in kernel (discarding checker/term.mli)
*** Warning: modops.mli already found in kernel (discarding checker/modops.mli)
*** Warning: main.ml already found in tools/coqdoc (discarding checker/main.ml)
*** Warning: typeops.mli already found in kernel (discarding checker/typeops.mli)
*** Warning: inductive.mli already found in kernel (discarding checker/inductive.mli)
*** Warning: indtypes.mli already found in kernel (discarding checker/indtypes.mli)
*** Warning: indtypes.ml already found in kernel (discarding checker/indtypes.ml)
*** Warning: safe_typing.ml already found in kernel (discarding checker/safe_typing.ml)
*** Warning: typeops.ml already found in kernel (discarding checker/typeops.ml)
*** Warning: modops.ml already found in kernel (discarding checker/modops.ml)
CAMLP4DEPS grammar/argextend.ml4
CAMLP4DEPS grammar/tacextend.ml4
CAMLP4DEPS grammar/q_coqast.ml4
CAMLP4DEPS grammar/q_constr.ml4
CAMLP4DEPS grammar/q_util.ml4
CAMLP4DEPS grammar/vernacextend.ml4
CAMLP4DEPS ide/project_file.ml4
CAMLP4DEPS ide/coqide_main.ml4
CAMLP4DEPS parsing/compat.ml4
CAMLP4DEPS parsing/g_proofs.ml4
CAMLP4DEPS parsing/g_constr.ml4
CAMLP4DEPS parsing/pcoq.ml4
CAMLP4DEPS parsing/g_vernac.ml4
CAMLP4DEPS parsing/g_prim.ml4
CAMLP4DEPS parsing/g_tactic.ml4
CAMLP4DEPS parsing/g_ltac.ml4
CAMLP4DEPS parsing/lexer.ml4
OCAMLDEP  toplevel/vernacinterp.mli
OCAMLDEP  toplevel/vernacentries.mli
OCAMLDEP  toplevel/vernac.mli
OCAMLDEP  toplevel/usage.mli
OCAMLDEP  toplevel/search.mli
OCAMLDEP  toplevel/record.mli
OCAMLDEP  toplevel/obligations.mli
OCAMLDEP  toplevel/mltop.mli
OCAMLDEP  toplevel/metasyntax.mli
OCAMLDEP  toplevel/locality.mli
OCAMLDEP  toplevel/indschemes.mli
OCAMLDEP  toplevel/ind_tables.mli
OCAMLDEP  toplevel/himsg.mli
OCAMLDEP  toplevel/discharge.mli
OCAMLDEP  toplevel/coqtop.mli
OCAMLDEP  toplevel/coqloop.mli
OCAMLDEP  toplevel/coqinit.mli
OCAMLDEP  toplevel/command.mli
OCAMLDEP  toplevel/classes.mli
OCAMLDEP  toplevel/class.mli
OCAMLDEP  toplevel/cerrors.mli
OCAMLDEP  toplevel/auto_ind_decl.mli
OCAMLDEP  toplevel/assumptions.mli
OCAMLDEP  tools/coqdoc/tokens.mli
OCAMLDEP  tools/coqdoc/output.mli
OCAMLDEP  tools/coqdoc/index.mli
OCAMLDEP  tools/coqdoc/cpretty.mli
OCAMLDEP  tools/coqdoc/alpha.mli
OCAMLDEP  tools/coqdep_lexer.mli
OCAMLDEP  tools/coqdep_common.mli
OCAMLDEP  tactics/term_dnet.mli
OCAMLDEP  tactics/tactics.mli
OCAMLDEP  tactics/tacticals.mli
OCAMLDEP  tactics/tactic_option.mli
OCAMLDEP  tactics/tactic_matching.mli
OCAMLDEP  tactics/tacsubst.mli
OCAMLDEP  tactics/tacinterp.mli
OCAMLDEP  tactics/tacintern.mli
OCAMLDEP  tactics/tacenv.mli
OCAMLDEP  tactics/taccoerce.mli
OCAMLDEP  tactics/rewrite.mli
OCAMLDEP  tactics/leminv.mli
OCAMLDEP  tactics/inv.mli
OCAMLDEP  tactics/hipattern.mli
OCAMLDEP  tactics/hints.mli
OCAMLDEP  tactics/geninterp.mli
OCAMLDEP  tactics/ftactic.mli
OCAMLDEP  tactics/extratactics.mli
OCAMLDEP  tactics/extraargs.mli
OCAMLDEP  tactics/evar_tactics.mli
OCAMLDEP  tactics/equality.mli
OCAMLDEP  tactics/eqschemes.mli
OCAMLDEP  tactics/eqdecide.mli
OCAMLDEP  tactics/elimschemes.mli
OCAMLDEP  tactics/elim.mli
OCAMLDEP  tactics/eauto.mli
OCAMLDEP  tactics/dnet.mli
OCAMLDEP  tactics/dn.mli
OCAMLDEP  tactics/contradiction.mli
OCAMLDEP  tactics/class_tactics.mli
OCAMLDEP  tactics/btermdn.mli
OCAMLDEP  tactics/autorewrite.mli
OCAMLDEP  tactics/auto.mli
OCAMLDEP  stm/workerPool.mli
OCAMLDEP  stm/vio_checking.mli
OCAMLDEP  stm/vernac_classifier.mli
OCAMLDEP  stm/vcs.mli
OCAMLDEP  stm/texmacspp.mli
OCAMLDEP  stm/tQueue.mli
OCAMLDEP  stm/stm.mli
OCAMLDEP  stm/spawned.mli
OCAMLDEP  stm/lemmas.mli
OCAMLDEP  stm/dag.mli
OCAMLDEP  stm/coqworkmgrApi.mli
OCAMLDEP  stm/asyncTaskQueue.mli
OCAMLDEP  proofs/tactic_debug.mli
OCAMLDEP  proofs/tacmach.mli
OCAMLDEP  proofs/refiner.mli
OCAMLDEP  proofs/redexpr.mli
OCAMLDEP  proofs/proofview_monad.mli
OCAMLDEP  proofs/proofview.mli
OCAMLDEP  proofs/proof_using.mli
OCAMLDEP  proofs/proof_type.mli
OCAMLDEP  proofs/proof_global.mli
OCAMLDEP  proofs/proof.mli
OCAMLDEP  proofs/pfedit.mli
OCAMLDEP  proofs/logic_monad.mli
OCAMLDEP  proofs/logic.mli
OCAMLDEP  proofs/goal.mli
OCAMLDEP  proofs/evar_refiner.mli
OCAMLDEP  proofs/clenvtac.mli
OCAMLDEP  proofs/clenv.mli
OCAMLDEP  printing/richprinter.mli
OCAMLDEP  printing/printmodsig.mli
OCAMLDEP  printing/printmod.mli
OCAMLDEP  printing/printer.mli
OCAMLDEP  printing/prettyp.mli
OCAMLDEP  printing/ppvernacsig.mli
OCAMLDEP  printing/ppvernac.mli
OCAMLDEP  printing/pputils.mli
OCAMLDEP  printing/pptacticsig.mli
OCAMLDEP  printing/pptactic.mli
OCAMLDEP  printing/ppconstrsig.mli
OCAMLDEP  printing/ppconstr.mli
OCAMLDEP  printing/ppannotation.mli
OCAMLDEP  printing/miscprint.mli
OCAMLDEP  printing/genprint.mli
OCAMLDEP  pretyping/vnorm.mli
OCAMLDEP  pretyping/unification.mli
OCAMLDEP  pretyping/typing.mli
OCAMLDEP  pretyping/typeclasses_errors.mli
OCAMLDEP  pretyping/typeclasses.mli
OCAMLDEP  pretyping/termops.mli
OCAMLDEP  pretyping/tacred.mli
OCAMLDEP  pretyping/retyping.mli
OCAMLDEP  pretyping/reductionops.mli
OCAMLDEP  pretyping/redops.mli
OCAMLDEP  pretyping/recordops.mli
OCAMLDEP  pretyping/program.mli
OCAMLDEP  pretyping/pretyping.mli
OCAMLDEP  pretyping/pretype_errors.mli
OCAMLDEP  pretyping/patternops.mli
OCAMLDEP  pretyping/nativenorm.mli
OCAMLDEP  pretyping/namegen.mli
OCAMLDEP  pretyping/miscops.mli
OCAMLDEP  pretyping/locusops.mli
OCAMLDEP  pretyping/inductiveops.mli
OCAMLDEP  pretyping/indrec.mli
OCAMLDEP  pretyping/glob_ops.mli
OCAMLDEP  pretyping/find_subterm.mli
OCAMLDEP  pretyping/evd.mli
OCAMLDEP  pretyping/evarutil.mli
OCAMLDEP  pretyping/evarsolve.mli
OCAMLDEP  pretyping/evarconv.mli
OCAMLDEP  pretyping/detyping.mli
OCAMLDEP  pretyping/constr_matching.mli
OCAMLDEP  pretyping/coercion.mli
OCAMLDEP  pretyping/classops.mli
OCAMLDEP  pretyping/cbv.mli
OCAMLDEP  pretyping/cases.mli
OCAMLDEP  pretyping/arguments_renaming.mli
OCAMLDEP  plugins/rtauto/refl_tauto.mli
OCAMLDEP  plugins/rtauto/proof_search.mli
OCAMLDEP  plugins/romega/const_omega.mli
OCAMLDEP  plugins/nsatz/utile.mli
OCAMLDEP  plugins/nsatz/polynom.mli
OCAMLDEP  plugins/micromega/sos.mli
OCAMLDEP  plugins/micromega/micromega.mli
OCAMLDEP  plugins/funind/recdef.mli
OCAMLDEP  plugins/funind/indfun_common.mli
OCAMLDEP  plugins/funind/indfun.mli
OCAMLDEP  plugins/funind/glob_termops.mli
OCAMLDEP  plugins/funind/glob_term_to_relation.mli
OCAMLDEP  plugins/funind/functional_principles_types.mli
OCAMLDEP  plugins/funind/functional_principles_proofs.mli
OCAMLDEP  plugins/firstorder/unify.mli
OCAMLDEP  plugins/firstorder/sequent.mli
OCAMLDEP  plugins/firstorder/rules.mli
OCAMLDEP  plugins/firstorder/instances.mli
OCAMLDEP  plugins/firstorder/ground.mli
OCAMLDEP  plugins/firstorder/formula.mli
OCAMLDEP  plugins/extraction/table.mli
OCAMLDEP  plugins/extraction/scheme.mli
OCAMLDEP  plugins/extraction/ocaml.mli
OCAMLDEP  plugins/extraction/modutil.mli
OCAMLDEP  plugins/extraction/mlutil.mli
OCAMLDEP  plugins/extraction/miniml.mli
OCAMLDEP  plugins/extraction/json.mli
OCAMLDEP  plugins/extraction/haskell.mli
OCAMLDEP  plugins/extraction/extraction.mli
OCAMLDEP  plugins/extraction/extract_env.mli
OCAMLDEP  plugins/extraction/common.mli
OCAMLDEP  plugins/derive/derive.mli
OCAMLDEP  plugins/decl_mode/ppdecl_proof.mli
OCAMLDEP  plugins/decl_mode/decl_proof_instr.mli
OCAMLDEP  plugins/decl_mode/decl_mode.mli
OCAMLDEP  plugins/decl_mode/decl_interp.mli
OCAMLDEP  plugins/decl_mode/decl_expr.mli
OCAMLDEP  plugins/cc/cctac.mli
OCAMLDEP  plugins/cc/ccproof.mli
OCAMLDEP  plugins/cc/ccalgo.mli
OCAMLDEP  parsing/tok.mli
OCAMLDEP  parsing/pcoq.mli
OCAMLDEP  parsing/lexer.mli
OCAMLDEP  parsing/egramml.mli
OCAMLDEP  parsing/egramcoq.mli
OCAMLDEP  library/universes.mli
OCAMLDEP  library/summary.mli
OCAMLDEP  library/states.mli
OCAMLDEP  library/nametab.mli
OCAMLDEP  library/nameops.mli
OCAMLDEP  library/loadpath.mli
OCAMLDEP  library/library.mli
OCAMLDEP  library/libobject.mli
OCAMLDEP  library/libnames.mli
OCAMLDEP  library/lib.mli
OCAMLDEP  library/kindops.mli
OCAMLDEP  library/keys.mli
OCAMLDEP  library/impargs.mli
OCAMLDEP  library/heads.mli
OCAMLDEP  library/goptions.mli
OCAMLDEP  library/globnames.mli
OCAMLDEP  library/global.mli
OCAMLDEP  library/dischargedhypsmap.mli
OCAMLDEP  library/decls.mli
OCAMLDEP  library/declaremods.mli
OCAMLDEP  library/declare.mli
OCAMLDEP  lib/xml_printer.mli
OCAMLDEP  lib/xml_parser.mli
OCAMLDEP  lib/xml_lexer.mli
OCAMLDEP  lib/xml_datatype.mli
OCAMLDEP  lib/util.mli
OCAMLDEP  lib/unionfind.mli
OCAMLDEP  lib/unicode.mli
OCAMLDEP  lib/trie.mli
OCAMLDEP  lib/terminal.mli
OCAMLDEP  lib/system.mli
OCAMLDEP  lib/store.mli
OCAMLDEP  lib/stateid.mli
OCAMLDEP  lib/spawn.mli
OCAMLDEP  lib/serialize.mli
OCAMLDEP  lib/segmenttree.mli
OCAMLDEP  lib/rtree.mli
OCAMLDEP  lib/richpp.mli
OCAMLDEP  lib/remoteCounter.mli
OCAMLDEP  lib/profile.mli
OCAMLDEP  lib/predicate.mli
OCAMLDEP  lib/ppstyle.mli
OCAMLDEP  lib/pp_control.mli
OCAMLDEP  lib/pp.mli
OCAMLDEP  lib/option.mli
OCAMLDEP  lib/monad.mli
OCAMLDEP  lib/loc.mli
OCAMLDEP  lib/int.mli
OCAMLDEP  lib/iStream.mli
OCAMLDEP  lib/hook.mli
OCAMLDEP  lib/heap.mli
OCAMLDEP  lib/hashset.mli
OCAMLDEP  lib/hashcons.mli
OCAMLDEP  lib/hMap.mli
OCAMLDEP  lib/genarg.mli
OCAMLDEP  lib/future.mli
OCAMLDEP  lib/flags.mli
OCAMLDEP  lib/feedback.mli
OCAMLDEP  lib/explore.mli
OCAMLDEP  lib/exninfo.mli
OCAMLDEP  lib/errors.mli
OCAMLDEP  lib/envars.mli
OCAMLDEP  lib/dyn.mli
OCAMLDEP  lib/deque.mli
OCAMLDEP  lib/control.mli
OCAMLDEP  lib/canary.mli
OCAMLDEP  lib/cUnix.mli
OCAMLDEP  lib/cThread.mli
OCAMLDEP  lib/cString.mli
OCAMLDEP  lib/cStack.mli
OCAMLDEP  lib/cSig.mli
OCAMLDEP  lib/cSet.mli
OCAMLDEP  lib/cObj.mli
OCAMLDEP  lib/cMap.mli
OCAMLDEP  lib/cList.mli
OCAMLDEP  lib/cEphemeron.mli
OCAMLDEP  lib/cArray.mli
OCAMLDEP  lib/bigint.mli
OCAMLDEP  lib/backtrace.mli
OCAMLDEP  lib/aux_file.mli
OCAMLDEP  kernel/vm.mli
OCAMLDEP  kernel/vconv.mli
OCAMLDEP  kernel/vars.mli
OCAMLDEP  kernel/univ.mli
OCAMLDEP  kernel/uint31.mli
OCAMLDEP  kernel/typeops.mli
OCAMLDEP  kernel/type_errors.mli
OCAMLDEP  kernel/term_typing.mli
OCAMLDEP  kernel/term.mli
OCAMLDEP  kernel/subtyping.mli
OCAMLDEP  kernel/sorts.mli
OCAMLDEP  kernel/safe_typing.mli
OCAMLDEP  kernel/retroknowledge.mli
OCAMLDEP  kernel/reduction.mli
OCAMLDEP  kernel/primitives.mli
OCAMLDEP  kernel/pre_env.mli
OCAMLDEP  kernel/opaqueproof.mli
OCAMLDEP  kernel/nativevalues.mli
OCAMLDEP  kernel/nativelibrary.mli
OCAMLDEP  kernel/nativelib.mli
OCAMLDEP  kernel/nativelambda.mli
OCAMLDEP  kernel/nativeinstr.mli
OCAMLDEP  kernel/nativeconv.mli
OCAMLDEP  kernel/nativecode.mli
OCAMLDEP  kernel/names.mli
OCAMLDEP  kernel/modops.mli
OCAMLDEP  kernel/mod_typing.mli
OCAMLDEP  kernel/mod_subst.mli
OCAMLDEP  kernel/inductive.mli
OCAMLDEP  kernel/indtypes.mli
OCAMLDEP  kernel/fast_typeops.mli
OCAMLDEP  kernel/evar.mli
OCAMLDEP  kernel/esubst.mli
OCAMLDEP  kernel/environ.mli
OCAMLDEP  kernel/entries.mli
OCAMLDEP  kernel/declareops.mli
OCAMLDEP  kernel/declarations.mli
OCAMLDEP  kernel/csymtable.mli
OCAMLDEP  kernel/cooking.mli
OCAMLDEP  kernel/conv_oracle.mli
OCAMLDEP  kernel/context.mli
OCAMLDEP  kernel/constr.mli
OCAMLDEP  kernel/closure.mli
OCAMLDEP  kernel/cemitcodes.mli
OCAMLDEP  kernel/cbytegen.mli
OCAMLDEP  kernel/cbytecodes.mli
OCAMLDEP  intf/vernacexpr.mli
OCAMLDEP  intf/tacexpr.mli
OCAMLDEP  intf/pattern.mli
OCAMLDEP  intf/notation_term.mli
OCAMLDEP  intf/misctypes.mli
OCAMLDEP  intf/locus.mli
OCAMLDEP  intf/glob_term.mli
OCAMLDEP  intf/genredexpr.mli
OCAMLDEP  intf/extend.mli
OCAMLDEP  intf/evar_kinds.mli
OCAMLDEP  intf/decl_kinds.mli
OCAMLDEP  intf/constrexpr.mli
OCAMLDEP  interp/topconstr.mli
OCAMLDEP  interp/syntax_def.mli
OCAMLDEP  interp/stdarg.mli
OCAMLDEP  interp/smartlocate.mli
OCAMLDEP  interp/reserve.mli
OCAMLDEP  interp/ppextend.mli
OCAMLDEP  interp/notation_ops.mli
OCAMLDEP  interp/notation.mli
OCAMLDEP  interp/modintern.mli
OCAMLDEP  interp/implicit_quantifiers.mli
OCAMLDEP  interp/genintern.mli
OCAMLDEP  interp/dumpglob.mli
OCAMLDEP  interp/coqlib.mli
OCAMLDEP  interp/constrintern.mli
OCAMLDEP  interp/constrextern.mli
OCAMLDEP  interp/constrexpr_ops.mli
OCAMLDEP  interp/constrarg.mli
OCAMLDEP  ide/xmlprotocol.mli
OCAMLDEP  ide/wg_Segment.mli
OCAMLDEP  ide/wg_ScriptView.mli
OCAMLDEP  ide/wg_ProofView.mli
OCAMLDEP  ide/wg_Notebook.mli
OCAMLDEP  ide/wg_MessageView.mli
OCAMLDEP  ide/wg_Find.mli
OCAMLDEP  ide/wg_Detachable.mli
OCAMLDEP  ide/wg_Completion.mli
OCAMLDEP  ide/wg_Command.mli
OCAMLDEP  ide/utils/okey.mli
OCAMLDEP  ide/utils/configwin.mli
OCAMLDEP  ide/utils/config_file.mli
OCAMLDEP  ide/tags.mli
OCAMLDEP  ide/session.mli
OCAMLDEP  ide/sentence.mli
OCAMLDEP  ide/preferences.mli
OCAMLDEP  ide/minilib.mli
OCAMLDEP  ide/interface.mli
OCAMLDEP  ide/ideutils.mli
OCAMLDEP  ide/fileOps.mli
OCAMLDEP  ide/document.mli
OCAMLDEP  ide/coqide.mli
OCAMLDEP  ide/coqOps.mli
OCAMLDEP  ide/coq.mli
OCAMLDEP  grammar/q_util.mli
OCAMLDEP  config/coq_config.mli
OCAMLDEP  checker/univ.mli
OCAMLDEP  checker/typeops.mli
OCAMLDEP  checker/type_errors.mli
OCAMLDEP  checker/term.mli
OCAMLDEP  checker/subtyping.mli
OCAMLDEP  checker/safe_typing.mli
OCAMLDEP  checker/reduction.mli
OCAMLDEP  checker/modops.mli
OCAMLDEP  checker/mod_checking.mli
OCAMLDEP  checker/inductive.mli
OCAMLDEP  checker/indtypes.mli
OCAMLDEP  checker/environ.mli
OCAMLDEP  checker/declarations.mli
OCAMLDEP  checker/closure.mli
OCAMLDEP  checker/cic.mli
OCAMLDEP  checker/check_stat.mli
OCAMLDEP  checker/analyze.mli
"/usr/bin/ocamlc.opt" -rectypes  -c tools/compat5.ml
"/usr/bin/ocamlc.opt" -rectypes  -c tools/compat5b.ml
CAMLP4O   grammar/argextend.ml4
OCAMLDEP  grammar/argextend.ml
CAMLP4O   grammar/tacextend.ml4
OCAMLDEP  grammar/tacextend.ml
CAMLP4O   grammar/q_coqast.ml4
OCAMLDEP  grammar/q_coqast.ml
CAMLP4O   grammar/q_constr.ml4
OCAMLDEP  grammar/q_constr.ml
CAMLP4O   grammar/q_util.ml4
OCAMLDEP  grammar/q_util.ml
CAMLP4O   grammar/vernacextend.ml4
OCAMLDEP  grammar/vernacextend.ml
CAMLP4O   ide/project_file.ml4
OCAMLDEP  ide/project_file.ml
CAMLP4O   ide/coqide_main.ml4
OCAMLDEP  ide/coqide_main.ml
CAMLP4O   parsing/compat.ml4
OCAMLDEP  parsing/compat.ml
CAMLP4O   parsing/g_proofs.ml4
OCAMLDEP  parsing/g_proofs.ml
CAMLP4O   parsing/g_constr.ml4
OCAMLDEP  parsing/g_constr.ml
CAMLP4O   parsing/pcoq.ml4
OCAMLDEP  parsing/pcoq.ml
CAMLP4O   parsing/g_vernac.ml4
OCAMLDEP  parsing/g_vernac.ml
CAMLP4O   parsing/g_prim.ml4
OCAMLDEP  parsing/g_prim.ml
CAMLP4O   parsing/g_tactic.ml4
OCAMLDEP  parsing/g_tactic.ml
CAMLP4O   parsing/g_ltac.ml4
OCAMLDEP  parsing/g_ltac.ml
CAMLP4O   parsing/lexer.ml4
OCAMLDEP  parsing/lexer.ml
OCAMLDEP  plugins/quote/quote_plugin_mod.ml
OCAMLDEP  plugins/extraction/extraction_plugin_mod.ml
OCAMLDEP  plugins/setoid_ring/newring_plugin_mod.ml
OCAMLDEP  plugins/btauto/btauto_plugin_mod.ml
OCAMLDEP  plugins/micromega/micromega_plugin_mod.ml
OCAMLDEP  plugins/romega/romega_plugin_mod.ml
OCAMLDEP  plugins/nsatz/nsatz_plugin_mod.ml
OCAMLDEP  plugins/firstorder/ground_plugin_mod.ml
OCAMLDEP  plugins/funind/recdef_plugin_mod.ml
OCAMLDEP  plugins/fourier/fourier_plugin_mod.ml
OCAMLDEP  plugins/cc/cc_plugin_mod.ml
OCAMLDEP  plugins/rtauto/rtauto_plugin_mod.ml
OCAMLDEP  plugins/syntax/numbers_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/r_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/z_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/ascii_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLDEP  plugins/syntax/string_syntax_plugin_mod.ml
OCAMLDEP  plugins/omega/omega_plugin_mod.ml
OCAMLDEP  plugins/derive/derive_plugin_mod.ml
OCAMLDEP  plugins/decl_mode/decl_mode_plugin_mod.ml
OCAMLDEP  kernel/copcodes.ml
OCAMLDEP  tools/tolink.ml
OCAMLDEP  lib/xml_lexer.ml
OCAMLDEP  tools/gallina_lexer.ml
OCAMLDEP  tools/coqdep_lexer.ml
OCAMLDEP  tools/coqdoc/cpretty.ml
OCAMLDEP  tools/coqwc.ml
OCAMLDEP  ide/utf8_convert.ml
OCAMLDEP  ide/coq_lex.ml
OCAMLDEP  ide/config_lexer.ml
OCAMLDEP  dev/vm_printers.ml
OCAMLDEP  dev/dynlink.ml
OCAMLDEP  dev/top_printers.ml
OCAMLDEP  dev/db_printers.ml
OCAMLDEP  checker/validate.ml
OCAMLDEP  checker/check_stat.ml
OCAMLDEP  checker/values.ml
OCAMLDEP  checker/modops.ml
OCAMLDEP  checker/typeops.ml
OCAMLDEP  checker/safe_typing.ml
OCAMLDEP  checker/indtypes.ml
OCAMLDEP  checker/main.ml
OCAMLDEP  checker/closure.ml
OCAMLDEP  checker/reduction.ml
OCAMLDEP  checker/analyze.ml
OCAMLDEP  checker/mod_checking.ml
OCAMLDEP  checker/print.ml
OCAMLDEP  checker/votour.ml
OCAMLDEP  checker/type_errors.ml
OCAMLDEP  checker/declarations.ml
OCAMLDEP  checker/environ.ml
OCAMLDEP  checker/univ.ml
OCAMLDEP  checker/checker.ml
OCAMLDEP  checker/subtyping.ml
OCAMLDEP  checker/term.ml
OCAMLDEP  checker/inductive.ml
OCAMLDEP  checker/check.ml
OCAMLDEP  kernel/nativelambda.ml
OCAMLDEP  kernel/modops.ml
OCAMLDEP  kernel/sorts.ml
OCAMLDEP  kernel/esubst.ml
OCAMLDEP  kernel/constr.ml
OCAMLDEP  kernel/typeops.ml
OCAMLDEP  kernel/term_typing.ml
OCAMLDEP  kernel/safe_typing.ml
OCAMLDEP  kernel/indtypes.ml
OCAMLDEP  kernel/csymtable.ml
OCAMLDEP  kernel/cbytegen.ml
OCAMLDEP  kernel/conv_oracle.ml
OCAMLDEP  kernel/cooking.ml
OCAMLDEP  kernel/declareops.ml
OCAMLDEP  kernel/nativelibrary.ml
OCAMLDEP  kernel/closure.ml
OCAMLDEP  kernel/nativeconv.ml
OCAMLDEP  kernel/mod_subst.ml
OCAMLDEP  kernel/reduction.ml
OCAMLDEP  kernel/mod_typing.ml
OCAMLDEP  kernel/retroknowledge.ml
OCAMLDEP  kernel/cbytecodes.ml
OCAMLDEP  kernel/nativecode.ml
OCAMLDEP  kernel/fast_typeops.ml
OCAMLDEP  kernel/uint31.ml
OCAMLDEP  kernel/vars.ml
OCAMLDEP  kernel/primitives.ml
OCAMLDEP  kernel/vconv.ml
OCAMLDEP  kernel/evar.ml
OCAMLDEP  kernel/cemitcodes.ml
OCAMLDEP  kernel/type_errors.ml
OCAMLDEP  kernel/names.ml
OCAMLDEP  kernel/vm.ml
OCAMLDEP  kernel/opaqueproof.ml
OCAMLDEP  kernel/nativelib.ml
OCAMLDEP  kernel/environ.ml
OCAMLDEP  kernel/context.ml
OCAMLDEP  kernel/pre_env.ml
OCAMLDEP  kernel/nativevalues.ml
OCAMLDEP  kernel/univ.ml
OCAMLDEP  kernel/subtyping.ml
OCAMLDEP  kernel/term.ml
OCAMLDEP  kernel/inductive.ml
OCAMLDEP  tactics/tactic_option.ml
OCAMLDEP  tactics/elimschemes.ml
OCAMLDEP  tactics/term_dnet.ml
OCAMLDEP  tactics/tacinterp.ml
OCAMLDEP  tactics/dnet.ml
OCAMLDEP  tactics/geninterp.ml
OCAMLDEP  tactics/autorewrite.ml
OCAMLDEP  tactics/ftactic.ml
OCAMLDEP  tactics/equality.ml
OCAMLDEP  tactics/auto.ml
OCAMLDEP  tactics/class_tactics.ml
OCAMLDEP  tactics/taccoerce.ml
OCAMLDEP  tactics/tactics.ml
OCAMLDEP  tactics/leminv.ml
OCAMLDEP  tactics/eqschemes.ml
OCAMLDEP  tactics/eqdecide.ml
OCAMLDEP  tactics/tacintern.ml
OCAMLDEP  tactics/contradiction.ml
OCAMLDEP  tactics/btermdn.ml
OCAMLDEP  tactics/tacticals.ml
OCAMLDEP  tactics/rewrite.ml
OCAMLDEP  tactics/inv.ml
OCAMLDEP  tactics/evar_tactics.ml
OCAMLDEP  tactics/tactic_matching.ml
OCAMLDEP  tactics/tacenv.ml
OCAMLDEP  tactics/dn.ml
OCAMLDEP  tactics/tacsubst.ml
OCAMLDEP  tactics/hints.ml
OCAMLDEP  tactics/elim.ml
OCAMLDEP  config/coq_config.ml
OCAMLDEP  lib/remoteCounter.ml
OCAMLDEP  lib/spawn.ml
OCAMLDEP  lib/rtree.ml
OCAMLDEP  lib/cStack.ml
OCAMLDEP  lib/predicate.ml
OCAMLDEP  lib/bigint.ml
OCAMLDEP  lib/control.ml
OCAMLDEP  lib/errors.ml
OCAMLDEP  lib/profile.ml
OCAMLDEP  lib/hashset.ml
OCAMLDEP  lib/xml_parser.ml
OCAMLDEP  lib/system.ml
OCAMLDEP  lib/canary.ml
OCAMLDEP  lib/hook.ml
OCAMLDEP  lib/option.ml
OCAMLDEP  lib/iStream.ml
OCAMLDEP  lib/unicode.ml
OCAMLDEP  lib/heap.ml
OCAMLDEP  lib/flags.ml
OCAMLDEP  lib/dyn.ml
OCAMLDEP  lib/serialize.ml
OCAMLDEP  lib/cMap.ml
OCAMLDEP  lib/util.ml
OCAMLDEP  lib/future.ml
OCAMLDEP  lib/unicodetable.ml
OCAMLDEP  lib/xml_printer.ml
OCAMLDEP  lib/hashcons.ml
OCAMLDEP  lib/cEphemeron.ml
OCAMLDEP  lib/cSet.ml
OCAMLDEP  lib/explore.ml
OCAMLDEP  lib/deque.ml
OCAMLDEP  lib/cThread.ml
OCAMLDEP  lib/unionfind.ml
OCAMLDEP  lib/pp_control.ml
OCAMLDEP  lib/backtrace.ml
OCAMLDEP  lib/genarg.ml
OCAMLDEP  lib/feedback.ml
OCAMLDEP  lib/trie.ml
OCAMLDEP  lib/terminal.ml
OCAMLDEP  lib/loc.ml
OCAMLDEP  lib/ppstyle.ml
OCAMLDEP  lib/envars.ml
OCAMLDEP  lib/int.ml
OCAMLDEP  lib/monad.ml
OCAMLDEP  lib/exninfo.ml
OCAMLDEP  lib/segmenttree.ml
OCAMLDEP  lib/richpp.ml
OCAMLDEP  lib/cUnix.ml
OCAMLDEP  lib/stateid.ml
OCAMLDEP  lib/aux_file.ml
OCAMLDEP  lib/cObj.ml
OCAMLDEP  lib/cString.ml
OCAMLDEP  lib/store.ml
OCAMLDEP  lib/cArray.ml
OCAMLDEP  lib/pp.ml
OCAMLDEP  lib/cList.ml
OCAMLDEP  lib/hMap.ml
OCAMLDEP  interp/constrextern.ml
OCAMLDEP  interp/constrarg.ml
OCAMLDEP  interp/implicit_quantifiers.ml
OCAMLDEP  interp/dumpglob.ml
OCAMLDEP  interp/smartlocate.ml
OCAMLDEP  interp/coqlib.ml
OCAMLDEP  interp/constrintern.ml
OCAMLDEP  interp/syntax_def.ml
OCAMLDEP  interp/genintern.ml
OCAMLDEP  interp/reserve.ml
OCAMLDEP  interp/ppextend.ml
OCAMLDEP  interp/notation.ml
OCAMLDEP  interp/topconstr.ml
OCAMLDEP  interp/stdarg.ml
OCAMLDEP  interp/notation_ops.ml
OCAMLDEP  interp/constrexpr_ops.ml
OCAMLDEP  interp/modintern.ml
OCAMLDEP  toplevel/discharge.ml
OCAMLDEP  toplevel/cerrors.ml
OCAMLDEP  toplevel/obligations.ml
OCAMLDEP  toplevel/class.ml
OCAMLDEP  toplevel/mltop.ml
OCAMLDEP  toplevel/vernac.ml
OCAMLDEP  toplevel/coqinit.ml
OCAMLDEP  toplevel/indschemes.ml
OCAMLDEP  toplevel/metasyntax.ml
OCAMLDEP  toplevel/coqtop.ml
OCAMLDEP  toplevel/ind_tables.ml
OCAMLDEP  toplevel/auto_ind_decl.ml
OCAMLDEP  toplevel/vernacinterp.ml
OCAMLDEP  toplevel/coqloop.ml
OCAMLDEP  toplevel/classes.ml
OCAMLDEP  toplevel/vernacentries.ml
OCAMLDEP  toplevel/assumptions.ml
OCAMLDEP  toplevel/search.ml
OCAMLDEP  toplevel/usage.ml
OCAMLDEP  toplevel/locality.ml
OCAMLDEP  toplevel/himsg.ml
OCAMLDEP  toplevel/record.ml
OCAMLDEP  toplevel/command.ml
OCAMLDEP  proofs/proof_type.ml
OCAMLDEP  proofs/clenvtac.ml
OCAMLDEP  proofs/logic_monad.ml
OCAMLDEP  proofs/refiner.ml
OCAMLDEP  proofs/proof.ml
OCAMLDEP  proofs/goal.ml
OCAMLDEP  proofs/proofview.ml
OCAMLDEP  proofs/proof_using.ml
OCAMLDEP  proofs/redexpr.ml
OCAMLDEP  proofs/evar_refiner.ml
OCAMLDEP  proofs/proof_global.ml
OCAMLDEP  proofs/tactic_debug.ml
OCAMLDEP  proofs/proofview_monad.ml
OCAMLDEP  proofs/pfedit.ml
OCAMLDEP  proofs/clenv.ml
OCAMLDEP  proofs/logic.ml
OCAMLDEP  proofs/tacmach.ml
OCAMLDEP  plugins/quote/quote.ml
OCAMLDEP  plugins/extraction/haskell.ml
OCAMLDEP  plugins/extraction/modutil.ml
OCAMLDEP  plugins/extraction/mlutil.ml
OCAMLDEP  plugins/extraction/scheme.ml
OCAMLDEP  plugins/extraction/table.ml
OCAMLDEP  plugins/extraction/extraction.ml
OCAMLDEP  plugins/extraction/extract_env.ml
OCAMLDEP  plugins/extraction/json.ml
OCAMLDEP  plugins/extraction/common.ml
OCAMLDEP  plugins/extraction/big.ml
OCAMLDEP  plugins/extraction/ocaml.ml
OCAMLDEP  plugins/btauto/refl_btauto.ml
OCAMLDEP  plugins/micromega/csdpcert.ml
OCAMLDEP  plugins/micromega/mutils.ml
OCAMLDEP  plugins/micromega/polynomial.ml
OCAMLDEP  plugins/micromega/sos.ml
OCAMLDEP  plugins/micromega/mfourier.ml
OCAMLDEP  plugins/micromega/sos_lib.ml
OCAMLDEP  plugins/micromega/sos_types.ml
OCAMLDEP  plugins/micromega/persistent_cache.ml
OCAMLDEP  plugins/micromega/coq_micromega.ml
OCAMLDEP  plugins/micromega/micromega.ml
OCAMLDEP  plugins/micromega/certificate.ml
OCAMLDEP  plugins/romega/const_omega.ml
OCAMLDEP  plugins/romega/refl_omega.ml
OCAMLDEP  plugins/nsatz/polynom.ml
OCAMLDEP  plugins/nsatz/utile.ml
OCAMLDEP  plugins/nsatz/ideal.ml
OCAMLDEP  plugins/firstorder/ground.ml
OCAMLDEP  plugins/firstorder/unify.ml
OCAMLDEP  plugins/firstorder/instances.ml
OCAMLDEP  plugins/firstorder/rules.ml
OCAMLDEP  plugins/firstorder/formula.ml
OCAMLDEP  plugins/firstorder/sequent.ml
OCAMLDEP  plugins/funind/merge.ml
OCAMLDEP  plugins/funind/functional_principles_proofs.ml
OCAMLDEP  plugins/funind/glob_termops.ml
OCAMLDEP  plugins/funind/functional_principles_types.ml
OCAMLDEP  plugins/funind/recdef.ml
OCAMLDEP  plugins/funind/indfun.ml
OCAMLDEP  plugins/funind/glob_term_to_relation.ml
OCAMLDEP  plugins/funind/indfun_common.ml
OCAMLDEP  plugins/funind/invfun.ml
OCAMLDEP  plugins/fourier/fourier.ml
OCAMLDEP  plugins/fourier/fourierR.ml
OCAMLDEP  plugins/cc/ccalgo.ml
OCAMLDEP  plugins/cc/cctac.ml
OCAMLDEP  plugins/cc/ccproof.ml
OCAMLDEP  plugins/rtauto/proof_search.ml
OCAMLDEP  plugins/rtauto/refl_tauto.ml
OCAMLDEP  plugins/syntax/nat_syntax.ml
OCAMLDEP  plugins/syntax/z_syntax.ml
OCAMLDEP  plugins/syntax/ascii_syntax.ml
OCAMLDEP  plugins/syntax/numbers_syntax.ml
OCAMLDEP  plugins/syntax/string_syntax.ml
OCAMLDEP  plugins/syntax/r_syntax.ml
OCAMLDEP  plugins/omega/omega.ml
OCAMLDEP  plugins/omega/coq_omega.ml
OCAMLDEP  plugins/derive/derive.ml
OCAMLDEP  plugins/decl_mode/ppdecl_proof.ml
OCAMLDEP  plugins/decl_mode/decl_interp.ml
OCAMLDEP  plugins/decl_mode/decl_mode.ml
OCAMLDEP  plugins/decl_mode/decl_proof_instr.ml
OCAMLDEP  tools/compat5.ml
OCAMLDEP  tools/gallina.ml
OCAMLDEP  tools/coqmktop.ml
OCAMLDEP  tools/coqdep_boot.ml
OCAMLDEP  tools/mkwinapp.ml
OCAMLDEP  tools/coqdep.ml
OCAMLDEP  tools/coqdep_common.ml
OCAMLDEP  tools/coqc.ml
OCAMLDEP  tools/fake_ide.ml
OCAMLDEP  tools/coqdoc/index.ml
OCAMLDEP  tools/coqdoc/main.ml
OCAMLDEP  tools/coqdoc/cdglobals.ml
OCAMLDEP  tools/coqdoc/output.ml
OCAMLDEP  tools/coqdoc/alpha.ml
OCAMLDEP  tools/coqdoc/tokens.ml
OCAMLDEP  tools/coq_tex.ml
OCAMLDEP  tools/coqworkmgr.ml
OCAMLDEP  tools/coq_makefile.ml
OCAMLDEP  tools/compat5b.ml
OCAMLDEP  library/keys.ml
OCAMLDEP  library/global.ml
OCAMLDEP  library/declare.ml
OCAMLDEP  library/dischargedhypsmap.ml
OCAMLDEP  library/lib.ml
OCAMLDEP  library/nametab.ml
OCAMLDEP  library/universes.ml
OCAMLDEP  library/globnames.ml
OCAMLDEP  library/decls.ml
OCAMLDEP  library/impargs.ml
OCAMLDEP  library/heads.ml
OCAMLDEP  library/states.ml
OCAMLDEP  library/nameops.ml
OCAMLDEP  library/kindops.ml
OCAMLDEP  library/libnames.ml
OCAMLDEP  library/loadpath.ml
OCAMLDEP  library/library.ml
OCAMLDEP  library/libobject.ml
OCAMLDEP  library/declaremods.ml
OCAMLDEP  library/goptions.ml
OCAMLDEP  library/summary.ml
OCAMLDEP  ide/wg_Detachable.ml
OCAMLDEP  ide/wg_Notebook.ml
OCAMLDEP  ide/session.ml
OCAMLDEP  ide/minilib.ml
OCAMLDEP  ide/coqide_ui.ml
OCAMLDEP  ide/tags.ml
OCAMLDEP  ide/macos_prehook.ml
OCAMLDEP  ide/coqOps.ml
OCAMLDEP  ide/wg_Command.ml
OCAMLDEP  ide/nanoPG.ml
OCAMLDEP  ide/sentence.ml
OCAMLDEP  ide/wg_ScriptView.ml
OCAMLDEP  ide/wg_ProofView.ml
OCAMLDEP  ide/wg_Segment.ml
OCAMLDEP  ide/ide_slave.ml
OCAMLDEP  ide/fileOps.ml
OCAMLDEP  ide/coq.ml
OCAMLDEP  ide/xmlprotocol.ml
OCAMLDEP  ide/coq_commands.ml
OCAMLDEP  ide/wg_Find.ml
OCAMLDEP  ide/utils/configwin.ml
OCAMLDEP  ide/utils/configwin_types.ml
OCAMLDEP  ide/utils/configwin_messages.ml
OCAMLDEP  ide/utils/configwin_ihm.ml
OCAMLDEP  ide/utils/configwin_keys.ml
OCAMLDEP  ide/utils/okey.ml
OCAMLDEP  ide/utils/config_file.ml
OCAMLDEP  ide/utils/editable_cells.ml
OCAMLDEP  ide/wg_Completion.ml
OCAMLDEP  ide/document.ml
OCAMLDEP  ide/ideutils.ml
OCAMLDEP  ide/preferences.ml
OCAMLDEP  ide/wg_MessageView.ml
OCAMLDEP  ide/gtk_parsing.ml
OCAMLDEP  ide/coqide.ml
OCAMLDEP  pretyping/arguments_renaming.ml
OCAMLDEP  pretyping/pretyping.ml
OCAMLDEP  pretyping/constr_matching.ml
OCAMLDEP  pretyping/patternops.ml
OCAMLDEP  pretyping/indrec.ml
OCAMLDEP  pretyping/cbv.ml
OCAMLDEP  pretyping/inductiveops.ml
OCAMLDEP  pretyping/classops.ml
OCAMLDEP  pretyping/evd.ml
OCAMLDEP  pretyping/redops.ml
OCAMLDEP  pretyping/evarconv.ml
OCAMLDEP  pretyping/typeclasses.ml
OCAMLDEP  pretyping/vnorm.ml
OCAMLDEP  pretyping/unification.ml
OCAMLDEP  pretyping/evarsolve.ml
OCAMLDEP  pretyping/coercion.ml
OCAMLDEP  pretyping/tacred.ml
OCAMLDEP  pretyping/typing.ml
OCAMLDEP  pretyping/glob_ops.ml
OCAMLDEP  pretyping/namegen.ml
OCAMLDEP  pretyping/miscops.ml
OCAMLDEP  pretyping/pretype_errors.ml
OCAMLDEP  pretyping/typeclasses_errors.ml
OCAMLDEP  pretyping/find_subterm.ml
OCAMLDEP  pretyping/detyping.ml
OCAMLDEP  pretyping/recordops.ml
OCAMLDEP  pretyping/evarutil.ml
OCAMLDEP  pretyping/retyping.ml
OCAMLDEP  pretyping/nativenorm.ml
OCAMLDEP  pretyping/reductionops.ml
OCAMLDEP  pretyping/locusops.ml
OCAMLDEP  pretyping/termops.ml
OCAMLDEP  pretyping/program.ml
OCAMLDEP  pretyping/cases.ml
OCAMLDEP  myocamlbuild.ml
OCAMLDEP  stm/lemmas.ml
OCAMLDEP  stm/dag.ml
OCAMLDEP  stm/asyncTaskQueue.ml
OCAMLDEP  stm/vcs.ml
OCAMLDEP  stm/vernac_classifier.ml
OCAMLDEP  stm/spawned.ml
OCAMLDEP  stm/coqworkmgrApi.ml
OCAMLDEP  stm/texmacspp.ml
OCAMLDEP  stm/vio_checking.ml
OCAMLDEP  stm/stm.ml
OCAMLDEP  stm/proofworkertop.ml
OCAMLDEP  stm/workerPool.ml
OCAMLDEP  stm/tQueue.ml
OCAMLDEP  stm/queryworkertop.ml
OCAMLDEP  stm/tacworkertop.ml
OCAMLDEP  configure.ml
OCAMLDEP  printing/miscprint.ml
OCAMLDEP  printing/printer.ml
OCAMLDEP  printing/ppconstr.ml
OCAMLDEP  printing/genprint.ml
OCAMLDEP  printing/richprinter.ml
OCAMLDEP  printing/pptactic.ml
OCAMLDEP  printing/pputils.ml
OCAMLDEP  printing/prettyp.ml
OCAMLDEP  printing/ppannotation.ml
OCAMLDEP  printing/ppvernac.ml
OCAMLDEP  printing/printmod.ml
OCAMLDEP  theories/Numbers/Natural/BigN/NMake_gen.ml
OCAMLDEP  parsing/tok.ml
OCAMLDEP  parsing/egramml.ml
OCAMLDEP  parsing/egramcoq.ml
OCAMLDEP  myocamlbuild_config.ml
OCAMLC    config/coq_config.mli
OCAMLC    config/coq_config.ml
OCAMLC    lib/hook.mli
OCAMLC    lib/hook.ml
OCAMLC    lib/terminal.mli
OCAMLC    lib/terminal.ml
OCAMLC    lib/canary.mli
OCAMLC    lib/canary.ml
OCAMLC    lib/hashset.mli
OCAMLC    lib/hashset.ml
OCAMLC    lib/hashcons.mli
OCAMLC    lib/hashcons.ml
File "lib/hashcons.ml", line 147, characters 4-74:
Warning 3: deprecated: [@@noalloc] should be used instead of "noalloc"
OCAMLC    lib/cSet.mli
OCAMLC    lib/cSet.ml
OCAMLC    lib/cSig.mli
OCAMLC    lib/cMap.mli
OCAMLC    lib/cMap.ml
OCAMLC    lib/int.mli
OCAMLC    lib/int.ml
OCAMLC    lib/hMap.mli
OCAMLC    lib/hMap.ml
OCAMLC    lib/option.mli
OCAMLC    lib/option.ml
OCAMLC    lib/store.mli
OCAMLC    lib/store.ml
OCAMLC    lib/exninfo.mli
OCAMLC    lib/exninfo.ml
OCAMLC    lib/backtrace.mli
OCAMLC    lib/backtrace.ml
OCAMLC    lib/pp_control.mli
OCAMLC    lib/pp_control.ml
File "lib/pp_control.ml", line 61, characters 22-33:
Error: This expression has type bytes -> int -> int -> unit
       but an expression was expected of type string -> int -> int -> unit
       Type bytes is not compatible with type string 
make[1]: *** [Makefile.build:978: lib/pp_control.cmo] Error 2
make[1]: Leaving directory '/home/pterjan/rpmbuild/BUILD/coq-8.5pl2'
make: *** [Makefile:158: submake] Error 2
error: Bad exit status from /home/pterjan/rpmbuild/tmp/rpm-tmp.58SscE (%build)


RPM build errors:
    Bad exit status from /home/pterjan/rpmbuild/tmp/rpm-tmp.58SscE (%build)
I: [iurt_root_command] ERROR: chroot