« Up

cfml 20181201 Error 🔥

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "armael.gueneau@inria.fr"
authors: "Arthur Charguéraud <arthur.chargueraud@inria.fr>"
homepage: "https://gitlab.inria.fr/charguer/cfml"
bug-reports: "https://gitlab.inria.fr/charguer/cfml/issues"
license: "CeCILL-B"
dev-repo: "git+https://gitlab.inria.fr/charguer/cfml.git"
build: [make "-j%{jobs}%"]
install: [make "install"]
synopsis: "A tool for proving OCaml programs in Separation Logic"
depends: [
  "ocaml" {>= "4.03.0" & < "4.08.0"}
  "ocamlbuild" {build}
  "pprint"
  "base-bytes"
  "coq" {>= "8.6"}
  "coq-tlc" {>= "20181116"}
]
url {
  src:
    "https://gitlab.inria.fr/charguer/cfml/repository/20181201/archive.tar.gz"
  checksum: "md5=0fd573617610a512381b58fe26a0edf6"
}

Lint

Command

true

Return code

0

Dry install 🏜️

Dry install with the current Coq version:

Command

opam install -y --show-action coq-cfml.20181201 coq.8.11.dev

Return code

0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command

true

Return code

0

Install dependencies

Command

opam list; echo; ulimit -Sv 4000000; timeout 2h opam install -y --deps-only coq-cfml.20181201 coq.8.11.dev

Return code

0

Duration

2 m 0 s

Install 🚀

Command

opam list; echo; ulimit -Sv 4000000; timeout 1h opam install -y -v coq-cfml.20181201 coq.8.11.dev

Return code

7936

Duration

1 m 0 s

Output

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-bytes          base        Bytes library distributed with the OCaml compiler
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
coq-tlc             20181116    A general-purpose alternative to Coq's standard library
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.05.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0      Official 4.05.0 release
ocaml-config        1           OCaml Switch Configuration
ocamlbuild          0.14.0      OCamlbuild is a build system with builtin rules to easily build most OCaml projects.
ocamlfind           1.8.1       A library manager for OCaml
pprint              20180528    A pretty-printing combinator library and rendering engine
[NOTE] Package coq is already installed (current version is 8.11.dev).
The following actions will be performed:
  - install coq-cfml 20181201
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/1: [coq-cfml.20181201: http]
[coq-cfml.20181201] downloaded from https://gitlab.inria.fr/charguer/cfml/repository/20181201/archive.tar.gz
Processing  1/1:
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Processing  1/2: [coq-cfml: make]
+ /home/bench/.opam/opam-init/hooks/sandbox.sh "build" "make" "-j4" (CWD=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201)
- make CFML=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201 -C lib/coq proof
- rm -f generator/cfml_config.ml
- sed -e 's|@@PREFIX@@|/home/bench/.opam/ocaml-base-compiler.4.05.0|' \
-     -e 's|@@BINDIR@@|/home/bench/.opam/ocaml-base-compiler.4.05.0/bin|' \
-     -e 's|@@LIBDIR@@|/home/bench/.opam/ocaml-base-compiler.4.05.0/lib/cfml|' \
-     generator/cfml_config.ml.in > generator/cfml_config.ml
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq'
- make -C generator
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator'
- ocamlbuild -j 4 -classic-display -I lex -I parsing -I typing -I utils -cflags "-g" -lflags "-g" -use-ocamlfind -package pprint main.native makecmj.native
- ocamlfind ocamldep -package pprint -modules main.ml > main.ml.depends
- ocamlfind ocamldep -package pprint -modules cfml_config.ml > cfml_config.ml.depends
- ocamlfind ocamldep -package pprint -modules characteristic.mli > characteristic.mli.depends
- ocamlfind ocamldep -package pprint -modules formula.mli > formula.mli.depends
- ocamlfind ocamldep -package pprint -modules coq.ml > coq.ml.depends
- ocamlfind ocamldep -package pprint -modules mytools.mli > mytools.mli.depends
- ocamlfind ocamldep -package pprint -modules parsing/location.mli > parsing/location.mli.depends
- ocamlfind ocamldep -package pprint -modules utils/warnings.mli > utils/warnings.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/warnings.cmi utils/warnings.mli
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/location.cmi parsing/location.mli
- ocamlfind ocamldep -package pprint -modules renaming.ml > renaming.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/clflags.mli > utils/clflags.mli.depends
- Compiling Shared...
- ocamlfind ocamldep -package pprint -modules typing/ident.mli > typing/ident.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o mytools.cmi mytools.mli
- ocamlfind ocamldep -package pprint -modules typing/path.mli > typing/path.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/ident.cmi typing/ident.mli
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/clflags.cmi utils/clflags.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/path.cmi typing/path.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o renaming.cmo renaming.ml
- + ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o renaming.cmo renaming.ml
- File "renaming.ml", line 241, characters 4-20:
- Warning 3: deprecated: String.uppercase
- Use String.uppercase_ascii instead.
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o coq.cmo coq.ml
- ocamlfind ocamldep -package pprint -modules typing/typedtree.mli > typing/typedtree.mli.depends
- ocamlfind ocamldep -package pprint -modules parsing/asttypes.mli > parsing/asttypes.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/env.mli > typing/env.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/annot.mli > typing/annot.mli.depends
- ocamlfind ocamldep -package pprint -modules utils/consistbl.mli > utils/consistbl.mli.depends
- ocamlfind ocamldep -package pprint -modules parsing/longident.mli > parsing/longident.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/types.mli > typing/types.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/asttypes.cmi parsing/asttypes.mli
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 8, characters 0-45:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 10, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamldep -package pprint -modules typing/primitive.mli > typing/primitive.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/primitive.cmi typing/primitive.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/annot.cmi typing/annot.mli
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/consistbl.cmi utils/consistbl.mli
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/longident.cmi parsing/longident.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/types.cmi typing/types.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/env.cmi typing/env.mli
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 206, characters 0-64:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope blocker_scope.". [undeclared-scope,deprecated]
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o formula.cmi formula.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typedtree.cmi typing/typedtree.mli
- ocamlfind ocamldep -package pprint -modules formula_to_coq.mli > formula_to_coq.mli.depends
- ocamlfind ocamldep -package pprint -modules normalize.mli > normalize.mli.depends
- ocamlfind ocamldep -package pprint -modules parsing/parsetree.mli > parsing/parsetree.mli.depends
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 353, characters 0-83:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope func.". [undeclared-scope,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 358, characters 0-28:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 377, characters 0-28:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/parsetree.cmi parsing/parsetree.mli
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 401, characters 0-22:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 406, characters 0-33:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/Shared.v", line 434, characters 0-24:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamldep -package pprint -modules parse_type.mli > parse_type.mli.depends
- ocamlfind ocamldep -package pprint -modules print_coq.mli > print_coq.mli.depends
- ocamlfind ocamldep -package pprint -modules print_past.mli > print_past.mli.depends
- Compiling CFHeaps...
- ocamlfind ocamldep -package pprint -modules print_tast.mli > print_tast.mli.depends
- ocamlfind ocamldep -package pprint -modules settings.mli > settings.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/typetexp.mli > typing/typetexp.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o cfml_config.cmo cfml_config.ml
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o characteristic.cmi characteristic.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o formula_to_coq.cmi formula_to_coq.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o normalize.cmi normalize.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o parse_type.cmi parse_type.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_coq.cmi print_coq.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_past.cmi print_past.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_tast.cmi print_tast.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o settings.cmi settings.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typetexp.cmi typing/typetexp.mli
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o main.cmo main.ml
- ocamlfind ocamldep -package pprint -modules characteristic.ml > characteristic.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/clflags.ml > utils/clflags.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/config.ml > utils/config.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/config.mli > utils/config.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/config.cmi utils/config.mli
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/config.cmx utils/config.ml
- ocamlfind ocamldep -package pprint -modules mytools.ml > mytools.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/location.ml > parsing/location.ml.depends
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 2, characters 0-54:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamllex.opt -q parsing/linenum.mll
- ocamlfind ocamldep -package pprint -modules parsing/linenum.ml > parsing/linenum.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/linenum.mli > parsing/linenum.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/linenum.cmi parsing/linenum.mli
- ocamlfind ocamldep -package pprint -modules utils/misc.ml > utils/misc.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/misc.mli > utils/misc.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/misc.cmi utils/misc.mli
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/misc.cmx utils/misc.ml
- + ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/misc.cmx utils/misc.ml
- File "utils/misc.ml", line 95, characters 14-33:
- Warning 3: deprecated: String.uncapitalize
- Use String.uncapitalize_ascii instead.
- File "utils/misc.ml", line 131, characters 13-26:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- File "utils/misc.ml", line 138, characters 13-26:
- Warning 3: deprecated: String.create
- Use Bytes.create instead.
- ocamlfind ocamldep -package pprint -modules utils/terminfo.ml > utils/terminfo.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/terminfo.mli > utils/terminfo.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/terminfo.cmi utils/terminfo.mli
- ocamlfind ocamldep -package pprint -modules utils/warnings.ml > utils/warnings.ml.depends
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 139, characters 0-124:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope state_scope.". [undeclared-scope,deprecated]
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/linenum.cmx parsing/linenum.ml
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/terminfo.cmx utils/terminfo.ml
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/warnings.cmx utils/warnings.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 187, characters 0-78:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- + ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/warnings.cmx utils/warnings.ml
- File "utils/warnings.ml", line 159, characters 30-44:
- Warning 3: deprecated: Char.lowercase
- Use Char.lowercase_ascii instead.
- File "utils/warnings.ml", line 176, characters 32-46:
- Warning 3: deprecated: Char.lowercase
- Use Char.lowercase_ascii instead.
- File "utils/warnings.ml", line 275, characters 4-48:
- Warning 3: deprecated: Format.pp_get_all_formatter_output_functions
- Use Format.pp_get_formatter_out_functions instead.
- File "utils/warnings.ml", line 278, characters 2-46:
- Warning 3: deprecated: Format.pp_set_all_formatter_output_functions
- Use Format.pp_set_formatter_out_functions instead.
- File "utils/warnings.ml", line 281, characters 2-46:
- Warning 3: deprecated: Format.pp_set_all_formatter_output_functions
- Use Format.pp_set_formatter_out_functions instead.
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/location.cmx parsing/location.ml
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/clflags.cmx utils/clflags.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 256, characters 0-57:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamldep -package pprint -modules typing/ident.ml > typing/ident.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o mytools.cmx mytools.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 365, characters 0-75:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- + ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o mytools.cmx mytools.ml
- File "mytools.ml", line 140, characters 19-33:
- Warning 3: deprecated: Char.uppercase
- Use Char.uppercase_ascii instead.
- File "mytools.ml", line 146, characters 19-33:
- Warning 3: deprecated: Char.uppercase
- Use Char.uppercase_ascii instead.
- ocamlfind ocamldep -package pprint -modules typing/path.ml > typing/path.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/ident.cmx typing/ident.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 456, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/path.cmx typing/path.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 535, characters 0-62:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope heap_scope.". [undeclared-scope,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 658, characters 0-56:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o renaming.cmx renaming.ml
- + ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o renaming.cmx renaming.ml
- File "renaming.ml", line 241, characters 4-20:
- Warning 3: deprecated: String.uppercase
- Use String.uppercase_ascii instead.
- ocamlfind ocamldep -package pprint -modules typing/ctype.ml > typing/ctype.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/ctype.mli > typing/ctype.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/ctype.cmi typing/ctype.mli
- ocamlfind ocamldep -package pprint -modules typing/btype.ml > typing/btype.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/btype.mli > typing/btype.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/btype.cmi typing/btype.mli
- ocamlfind ocamldep -package pprint -modules typing/types.ml > typing/types.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/primitive.ml > typing/primitive.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/primitive.cmx typing/primitive.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/types.cmx typing/types.ml
- ocamlfind ocamldep -package pprint -modules typing/env.ml > typing/env.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/btype.cmx typing/btype.ml
- ocamlfind ocamldep -package pprint -modules utils/consistbl.ml > utils/consistbl.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/datarepr.ml > typing/datarepr.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/datarepr.mli > typing/datarepr.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/datarepr.cmi typing/datarepr.mli
- ocamlfind ocamldep -package pprint -modules typing/predef.ml > typing/predef.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/predef.mli > typing/predef.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/predef.cmi typing/predef.mli
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/predef.cmx typing/predef.ml
- ocamlfind ocamldep -package pprint -modules parsing/longident.ml > parsing/longident.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/subst.ml > typing/subst.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/subst.mli > typing/subst.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/subst.cmi typing/subst.mli
- ocamlfind ocamldep -package pprint -modules utils/tbl.ml > utils/tbl.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/tbl.mli > utils/tbl.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/tbl.cmi utils/tbl.mli
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/tbl.cmx utils/tbl.ml
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/consistbl.cmx utils/consistbl.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/datarepr.cmx typing/datarepr.ml
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/longident.cmx parsing/longident.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/subst.cmx typing/subst.ml
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/datarepr.cmx typing/datarepr.ml
- File "typing/datarepr.ml", line 73, characters 19-31:
- Warning 3: deprecated: Array.create
- Use Array.make instead.
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/env.cmx typing/env.ml
- ocamlfind ocamldep -package pprint -modules formula.ml > formula.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o coq.cmx coq.ml
- ocamlfind ocamldep -package pprint -modules print_tast.ml > print_tast.ml.depends
- ocamlfind ocamldep -package pprint -modules print_past.ml > print_past.ml.depends
- ocamlfind ocamldep -package pprint -modules print_type.ml > print_type.ml.depends
- ocamlfind ocamldep -package pprint -modules print_type.mli > print_type.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_type.cmi print_type.mli
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/ctype.cmx typing/ctype.ml
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/ctype.cmx typing/ctype.ml
- File "typing/ctype.ml", line 241, characters 5-14:
- Warning 3: deprecated: Sort.list
- Use List.sort instead.
- File "typing/ctype.ml", line 367, characters 22-31:
- Warning 3: deprecated: Sort.list
- Use List.sort instead.
- ocamlfind ocamldep -package pprint -modules typing/outcometree.mli > typing/outcometree.mli.depends
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_past.cmx print_past.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 2204, characters 0-29:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamldep -package pprint -modules typing/printtyp.ml > typing/printtyp.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/printtyp.mli > typing/printtyp.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/outcometree.cmi typing/outcometree.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/printtyp.cmi typing/printtyp.mli
- ocamlfind ocamldep -package pprint -modules typing/oprint.ml > typing/oprint.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/oprint.mli > typing/oprint.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/oprint.cmi typing/oprint.mli
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/oprint.cmx typing/oprint.ml
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/oprint.cmx typing/oprint.ml
- File "typing/oprint.ml", line 103, characters 27-42:
- Warning 52: Code should not depend on the actual values of
- this constructor's arguments. They are only for information
- and may change in future versions. (See manual section 8.5)
- ocamlfind ocamldep -package pprint -modules typing/typedtree.ml > typing/typedtree.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/printtyp.cmx typing/printtyp.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typedtree.cmx typing/typedtree.ml
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/printtyp.cmx typing/printtyp.ml
- File "typing/printtyp.ml", line 434, characters 10-19:
- Warning 3: deprecated: Sort.list
- Use List.sort instead.
- File "typing/printtyp.ml", line 936, characters 4-57:
- Warning 57: Ambiguous or-pattern variables under guard;
- variable lab may match different arguments. (See manual section 8.5)
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_type.cmx print_type.ml
- ocamlfind ocamldep -package pprint -modules typing/typecore.ml > typing/typecore.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/typecore.mli > typing/typecore.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typecore.cmi typing/typecore.mli
- ocamlfind ocamldep -package pprint -modules typing/parmatch.ml > typing/parmatch.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/parmatch.mli > typing/parmatch.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/parmatch.cmi typing/parmatch.mli
- ocamlfind ocamldep -package pprint -modules typing/stypes.ml > typing/stypes.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/stypes.mli > typing/stypes.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/stypes.cmi typing/stypes.mli
- ocamlfind ocamldep -package pprint -modules typing/typetexp.ml > typing/typetexp.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/parmatch.cmx typing/parmatch.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/stypes.cmx typing/stypes.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typetexp.cmx typing/typetexp.ml
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/parmatch.cmx typing/parmatch.ml
- File "typing/parmatch.ml", line 55, characters 2-11:
- Warning 3: deprecated: Sort.list
- Use List.sort instead.
- File "typing/parmatch.ml", line 144, characters 15-20:
- Warning 52: Code should not depend on the actual values of
- this constructor's arguments. They are only for information
- and may change in future versions. (See manual section 8.5)
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o formula.cmx formula.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_tast.cmx print_tast.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typecore.cmx typing/typecore.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeaps.v", line 2588, characters 0-28:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- Compiling CFApp...
- ocamlfind ocamldep -package pprint -modules formula_to_coq.ml > formula_to_coq.ml.depends
- ocamlfind ocamldep -package pprint -modules normalize.ml > normalize.ml.depends
- ocamlfind ocamldep -package pprint -modules parse_type.ml > parse_type.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/ccomp.ml > utils/ccomp.ml.depends
- ocamlfind ocamldep -package pprint -modules utils/ccomp.mli > utils/ccomp.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/ccomp.cmi utils/ccomp.mli
- ocamlfind ocamldep -package pprint -modules parsing/parse.ml > parsing/parse.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/parse.mli > parsing/parse.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/parse.cmi parsing/parse.mli
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamllex.opt -q parsing/lexer.mll
- ocamlfind ocamldep -package pprint -modules parsing/lexer.ml > parsing/lexer.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/lexer.mli > parsing/lexer.mli.depends
- /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlyacc parsing/parser.mly
- + /home/bench/.opam/ocaml-base-compiler.4.05.0/bin/ocamlyacc parsing/parser.mly
- 1 rule never reduced
- ocamlfind ocamldep -package pprint -modules parsing/parser.mli > parsing/parser.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/parser.cmi parsing/parser.mli
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/lexer.cmi parsing/lexer.mli
- ocamlfind ocamldep -package pprint -modules parsing/parser.ml > parsing/parser.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/syntaxerr.ml > parsing/syntaxerr.ml.depends
- ocamlfind ocamldep -package pprint -modules parsing/syntaxerr.mli > parsing/syntaxerr.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/syntaxerr.cmi parsing/syntaxerr.mli
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/syntaxerr.cmx parsing/syntaxerr.ml
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/parser.cmx parsing/parser.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 2, characters 0-41:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 5, characters 0-49:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/lexer.cmx parsing/lexer.ml
- ocamlfind ocamldep -package pprint -modules typing/typemod.ml > typing/typemod.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/typemod.mli > typing/typemod.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/includemod.mli > typing/includemod.mli.depends
- ocamlfind ocamldep -package pprint -modules typing/includecore.mli > typing/includecore.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includecore.cmi typing/includecore.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includemod.cmi typing/includemod.mli
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typemod.cmi typing/typemod.mli
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 116, characters 0-29:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 127, characters 0-77:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope dynlist.". [undeclared-scope,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 162, characters 0-144:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope charac.". [undeclared-scope,deprecated]
- ocamlfind ocamldep -package pprint -modules typing/includemod.ml > typing/includemod.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/includeclass.ml > typing/includeclass.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/includeclass.mli > typing/includeclass.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includeclass.cmi typing/includeclass.mli
- ocamlfind ocamldep -package pprint -modules typing/includecore.ml > typing/includecore.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/mtype.ml > typing/mtype.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/mtype.mli > typing/mtype.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/mtype.cmi typing/mtype.mli
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includeclass.cmx typing/includeclass.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includecore.cmx typing/includecore.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/mtype.cmx typing/mtype.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 281, characters 0-23:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- ocamlfind ocamldep -package pprint -modules typing/typeclass.ml > typing/typeclass.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/typeclass.mli > typing/typeclass.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typeclass.cmi typing/typeclass.mli
- ocamlfind ocamldep -package pprint -modules typing/typedecl.ml > typing/typedecl.ml.depends
- ocamlfind ocamldep -package pprint -modules typing/typedecl.mli > typing/typedecl.mli.depends
- ocamlfind ocamlc -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typedecl.cmi typing/typedecl.mli
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typedecl.cmx typing/typedecl.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/includemod.cmx typing/includemod.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typeclass.cmx typing/typeclass.ml
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFApp.v", line 492, characters 0-98:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope record_scope.". [undeclared-scope,deprecated]
- ocamlfind ocamlopt -c -g -package pprint -I utils -I lex -I parsing -I typing -o utils/ccomp.cmx utils/ccomp.ml
- ocamlfind ocamlopt -c -g -package pprint -I parsing -I lex -I utils -I typing -o parsing/parse.cmx parsing/parse.ml
- ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typemod.cmx typing/typemod.ml
- Compiling CFPrint...
- + ocamlfind ocamlopt -c -g -package pprint -I typing -I lex -I utils -I parsing -o typing/typemod.cmx typing/typemod.ml
- File "typing/typemod.ml", line 1231, characters 23-40:
- Warning 3: deprecated: String.capitalize
- Use String.capitalize_ascii instead.
- ocamlfind ocamldep -package pprint -modules print_coq.ml > print_coq.ml.depends
- ocamlfind ocamldep -package pprint -modules settings.ml > settings.ml.depends
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o cfml_config.cmx cfml_config.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o characteristic.cmx characteristic.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o formula_to_coq.cmx formula_to_coq.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o normalize.cmx normalize.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o parse_type.cmx parse_type.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o print_coq.cmx print_coq.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o settings.cmx settings.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o main.cmx main.ml
- ocamlfind ocamlopt -g -linkpkg -package pprint -I utils -I parsing -I typing cfml_config.cmx utils/misc.cmx parsing/linenum.cmx utils/terminfo.cmx utils/warnings.cmx parsing/location.cmx mytools.cmx typing/ident.cmx typing/path.cmx utils/config.cmx utils/clflags.cmx renaming.cmx coq.cmx formula.cmx parsing/longident.cmx typing/primitive.cmx typing/types.cmx print_past.cmx typing/btype.cmx typing/predef.cmx typing/datarepr.cmx utils/tbl.cmx typing/subst.cmx utils/consistbl.cmx typing/env.cmx typing/ctype.cmx typing/oprint.cmx typing/printtyp.cmx typing/typedtree.cmx print_type.cmx print_tast.cmx typing/parmatch.cmx typing/stypes.cmx typing/typetexp.cmx typing/typecore.cmx characteristic.cmx formula_to_coq.cmx normalize.cmx parsing/syntaxerr.cmx parsing/parser.cmx parsing/lexer.cmx parsing/parse.cmx typing/includeclass.cmx typing/includecore.cmx typing/mtype.cmx typing/includemod.cmx typing/typedecl.cmx typing/typeclass.cmx typing/typemod.cmx utils/ccomp.cmx parse_type.cmx print_coq.cmx settings.cmx main.cmx -o main.native
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFPrint.v", line 2, characters 0-23:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFPrint.v", line 180, characters 0-75:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope tag_scope.". [undeclared-scope,deprecated]
- Compiling CFHeader...
- Compiling CFBuiltin...
- Compiling CFTactics...
- ocamlfind ocamldep -package pprint -modules makecmj.ml > makecmj.ml.depends
- ocamlfind ocamlc -c -g -package pprint -I lex -I utils -I parsing -I typing -o makecmj.cmo makecmj.ml
- ocamlfind ocamlopt -c -g -package pprint -I lex -I utils -I parsing -I typing -o makecmj.cmx makecmj.ml
- ocamlfind ocamlopt -g -linkpkg -package pprint -I utils -I parsing -I typing cfml_config.cmx utils/misc.cmx parsing/linenum.cmx utils/terminfo.cmx utils/warnings.cmx parsing/location.cmx mytools.cmx parsing/longident.cmx typing/ident.cmx typing/path.cmx utils/config.cmx utils/clflags.cmx renaming.cmx typing/primitive.cmx typing/types.cmx normalize.cmx parsing/syntaxerr.cmx parsing/parser.cmx parsing/lexer.cmx parsing/parse.cmx typing/btype.cmx typing/predef.cmx typing/datarepr.cmx utils/tbl.cmx typing/subst.cmx utils/consistbl.cmx typing/env.cmx typing/ctype.cmx typing/oprint.cmx typing/printtyp.cmx typing/includeclass.cmx typing/typedtree.cmx typing/includecore.cmx typing/mtype.cmx typing/includemod.cmx typing/parmatch.cmx typing/stypes.cmx typing/typetexp.cmx typing/typecore.cmx typing/typedecl.cmx typing/typeclass.cmx typing/typemod.cmx utils/ccomp.cmx parse_type.cmx settings.cmx makecmj.cmx -o makecmj.native
- # Parallel statistics: { count(total): 13(194), max: 10, min: 2, average(total): 3.692(1.180) }
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFHeader.v", line 12, characters 0-133:
- Warning: Declaring a scope implicitly is deprecated; use in advance an
- explicit "Declare Scope cfheader_scope.". [undeclared-scope,deprecated]
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator'
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFBuiltin.v", line 2, characters 0-23:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFTactics.v", line 2, characters 0-38:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- Compiling CFLib...
- Compiling CFDemos...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFDemos.v", line 2, characters 0-38:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFLib.v", line 1, characters 0-64:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- Compiling CFLibCredits...
- Compiling CFAsymptoticsDemos...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFLibCredits.v", line 1, characters 0-21:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq/CFAsymptoticsDemos.v", line 2, characters 0-21:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/coq'
- make CFMLC=/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator/main.native -C lib/stdlib
- make[1]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
- /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator/main.native  -nostdlib -nopervasives -I . /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives.ml || (rm -f /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives.cmj; exit 1)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator/main.native  -nostdlib -I . /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List.ml || (rm -f /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List.cmj; exit 1)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator/main.native  -nostdlib -I . /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys.ml || (rm -f /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys.cmj; exit 1)
- /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/generator/main.native  -nostdlib -I . /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array.ml || (rm -f /home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array.cmj; exit 1)
- make[2]: Entering directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
- Compiling Pervasives_ml...
- Compiling List_ml...
- Compiling Sys_ml...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 62, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 108, characters 0-85:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 170, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 220, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 261, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 286, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 337, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 380, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 408, characters 0-79:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 441, characters 0-85:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 487, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 533, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 590, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 647, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 675, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_ml.v", line 772, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- Compiling Array_ml...
- Compiling Pervasives_proof...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 137, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 378, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 516, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 525, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 622, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 654, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 781, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 895, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1052, characters 0-63:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1182, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1361, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys_ml.v", line 20, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys_ml.v", line 29, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys_ml.v", line 40, characters 0-85:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys_ml.v", line 51, characters 0-87:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- Compiling Sys_proof...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1491, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1621, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1753, characters 0-67:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 1885, characters 0-69:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 2011, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 2188, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 2446, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 2628, characters 0-63:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 2818, characters 0-67:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 3091, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 3334, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/List_ml.v", line 3682, characters 0-69:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 230, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 443, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 850, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1054, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1242, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 2, characters 0-21:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1559, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1629, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1861, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 1935, characters 0-63:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 2177, characters 0-61:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 2310, characters 0-67:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 2464, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_ml.v", line 2616, characters 0-73:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- Compiling Array_proof...
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 18, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 40, characters 0-75:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 57, characters 0-81:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 68, characters 0-65:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 75, characters 0-69:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Sys_proof.v", line 2, characters 0-21:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 93, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 94, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 106, characters 0-75:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 107, characters 0-75:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 138, characters 0-83:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 139, characters 0-69:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 140, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 141, characters 0-69:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 142, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 143, characters 0-67:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 187, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 188, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 189, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 230, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 231, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 232, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 233, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 234, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 235, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 236, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 237, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 287, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 288, characters 0-71:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 289, characters 0-77:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 2, characters 0-21:
- Warning:
- New coercion path [total_order_to_total_preorder; total_preorder_to_preorder] : total_order >-> preorder is ambiguous with existing 
- [total_order_order; order_to_preorder] : total_order >-> preorder.
- [ambiguous-paths,typechecker]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 311, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 312, characters 0-55:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 64, characters 0-70:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 77, characters 0-68:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 91, characters 0-62:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 105, characters 0-62:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 126, characters 0-64:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 134, characters 0-57:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.v", line 140, characters 26-27:
- Error:
- In environment
- i : int
- The term "i" has type "int" while it is expected to have type "nat".
- 
- /home/bench/.opam/ocaml-base-compiler.4.05.0/lib/coq/user-contrib/TLC/Makefile.coq:114: recipe for target '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.vo' failed
- make[2]: *** [/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Array_proof.vo] Error 1
- make[2]: *** Waiting for unfinished jobs....
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 360, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 361, characters 0-53:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 373, characters 0-59:
- Warning: Adding and removing hints in the core database implicitly is
- deprecated. Please specify a hint database.
- [implicit-core-hint-db,deprecated]
- make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
- Makefile:53: recipe for target 'all' failed
- make[1]: *** [all] Error 2
- make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
- Makefile:22: recipe for target 'all' failed
- make: *** [all] Error 2
[ERROR] The compilation of coq-cfml failed at "/home/bench/.opam/opam-init/hooks/sandbox.sh build make -j4".
#=== ERROR while compiling coq-cfml.20181201 ==================================#
# context              2.0.5 | linux/x86_64 | ocaml-base-compiler.4.05.0 | file:///home/bench/run/opam-coq-archive/released
# path                 ~/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201
# command              ~/.opam/opam-init/hooks/sandbox.sh build make -j4
# exit-code            2
# env-file             ~/.opam/log/coq-cfml-4705-865888.env
# output-file          ~/.opam/log/coq-cfml-4705-865888.out
### output ###
# [...]
# deprecated. Please specify a hint database.
# [implicit-core-hint-db,deprecated]
# File "/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib/Pervasives_proof.v", line 373, characters 0-59:
# Warning: Adding and removing hints in the core database implicitly is
# deprecated. Please specify a hint database.
# [implicit-core-hint-db,deprecated]
# make[2]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
# Makefile:53: recipe for target 'all' failed
# make[1]: *** [all] Error 2
# make[1]: Leaving directory '/home/bench/.opam/ocaml-base-compiler.4.05.0/.opam-switch/build/coq-cfml.20181201/lib/stdlib'
# Makefile:22: recipe for target 'all' failed
# make: *** [all] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build coq-cfml 20181201
+- 
- No changes have been performed
# Run eval $(opam env) to update the current shell environment
'opam install -y -v coq-cfml.20181201 coq.8.11.dev' failed.

Installation size

No files were installed.

Uninstall 🧹

Command

true

Return code

0

Missing removes

none

Wrong removes

none