proof-general warnings on coq-layer installation

compile.log

Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/acl2/acl2.el at Sun Dec 18 17:00:39 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/acl2/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/acl2/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/ccc/ccc.el at Sun Dec 18 17:00:39 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/ccc/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/ccc/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-abbrev.el at Sun Dec 18 17:00:39 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-autotest.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-compile-common.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-db.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-indent.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-local-vars.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-mmm.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-par-compile.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-par-test.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-seq-compile.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-smie.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-syntax.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-system.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq-unicode-tokens.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/coq.el at Sun Dec 18 17:00:39 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/coq/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/doc/docstring-magic.el at Sun Dec 18 17:00:39 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/doc/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/doc/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-assoc.el at Sun Dec 18 17:00:39 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-autotest.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-custom.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-goals.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-movie.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-pamacs.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-pbrpm.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-pgip.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-response.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-user.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-vars.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/pg-xml.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-autoloads.el at Sun Dec 18 17:00:39 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-auxmodes.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-config.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-depends.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-easy-config.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-faces.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-indent.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-maths-menu.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-menu.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-mmm.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-script.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-shell.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-site.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-splash.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-syntax.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-toolbar.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-tree.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-unicode-tokens.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-useropts.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof-utils.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/proof.el at Sun Dec 18 17:00:40 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/generic/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol-light/hol-light-autotest.el at Sun Dec 18 17:00:40 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol-light/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol-light/hol-light-unicode-tokens.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol-light/hol-light.el at Sun Dec 18 17:00:40 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol-light/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol98/hol98.el at Sun Dec 18 17:00:40 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol98/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/hol98/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/interface-setup.el at Sun Dec 18 17:00:40 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isabelle-system.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-autotest.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-find-theorems.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-keywords.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-mmm.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-profiling.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-syntax.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar-unicode-tokens.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/isar.el at Sun Dec 18 17:00:40 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/isar/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lego/lego-syntax.el at Sun Dec 18 17:00:40 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/lego/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lego/lego.el at Sun Dec 18 17:00:40 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/lego/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/bufhist.el at Sun Dec 18 17:00:40 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/holes.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/local-vars-list.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/maths-menu.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/pg-dev.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/pg-fontsets.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/proof-compat.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/scomint.el at Sun Dec 18 17:00:40 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/span.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/texi-docstring-magic.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/unicode-chars.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/unicode-tokens.el at Sun Dec 18 17:00:41 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/lib/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/pghaskell/pghaskell.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pghaskell/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pghaskell/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgocaml/pgocaml.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgocaml/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgocaml/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgshell/pgshell.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgshell/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/pgshell/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-extraction.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-font.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-fun.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-lang.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-outline.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-pbrpm.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-sym-lock.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox-tags.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/phox.el at Sun Dec 18 17:00:41 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/phox/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/twelf/twelf-font.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/twelf/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/twelf/twelf-old.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/twelf/twelf.el at Sun Dec 18 17:00:41 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/twelf/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ml4pg.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-auto.el at Sun Dec 18 17:00:41 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-class.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-cmds.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-compat.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-cweb.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-mason.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-mode.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-region.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-rpm.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-sample.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-univ.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-utils.el at Sun Dec 18 17:00:41 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/mmm-vars.el at Sun Dec 18 17:00:42 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/mmm/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/emacsbugs/visiblity-attempt.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/emacsbugs/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/emacsbugs/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/isar/new-parsing-test.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/isar/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/isar/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/lego/lego-site.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/lego/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/lego/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/testsuite/pg-pgip-test.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/testsuite/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/testsuite/pg-test.el at Sun Dec 18 17:00:42 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/etc/testsuite/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/demoisa/demoisa-easy.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/demoisa/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/demoisa/demoisa.el at Sun Dec 18 17:00:42 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/demoisa/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/lclam/lclam.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/lclam/’
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/lclam/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/plastic/plastic-syntax.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/plastic/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/plastic/plastic.el at Sun Dec 18 17:00:42 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/obsolete/plastic/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/auxiliary_files.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/feature_extraction.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/matlab_interaction.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/menus.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/save_lemmas.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/shortcuts.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/storage.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/weka.el at Sun Dec 18 17:00:42 2016
Leaving directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/coq/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/auxiliary_files.el at Sun Dec 18 17:00:42 2016
Entering directory ‘/Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/’

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/feature_extraction_2.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/matlab_interaction.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/menus.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/save_lemmas.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/shortcuts.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/storage.el at Sun Dec 18 17:00:42 2016

Compiling file /Users/vic/.emacs.d/elpa/proof-general-20161216.202/contrib/ML4PG/ssreflect/weka.el at Sun Dec 18 17:00:42 2016

Compiling no file at Sun Dec 18 17:00:42 2016
Error (bytecomp): Cannot open load file: No such file or directory, proof-easy-config [2 times]
Error (bytecomp): Cannot open load file: No such file or directory, proof
Error (bytecomp): Cannot open load file: No such file or directory, pg-autotest
Error (bytecomp): Cannot open load file: No such file or directory, proof-shell
Error (bytecomp): Cannot open load file: No such file or directory, proof-config
Error (bytecomp): Cannot open load file: No such file or directory, coq-syntax
Error (bytecomp): Cannot open load file: No such file or directory, local-vars-list
Error (bytecomp): Cannot open load file: No such file or directory, mmm-auto
Error (bytecomp): Cannot open load file: No such file or directory, proof-compat
Error (bytecomp): Cannot open load file: No such file or directory, coq-par-compile
Error (bytecomp): Cannot open load file: No such file or directory, proof-compat
Error (bytecomp): Cannot open load file: No such file or directory, coq-indent
Error (bytecomp): Cannot open load file: No such file or directory, proof-syntax
Error (bytecomp): Cannot open load file: No such file or directory, proof
Error (bytecomp): Cannot open load file: No such file or directory, proof-unicode-tokens
Error (bytecomp): Cannot open load file: No such file or directory, proof-compat
Error (bytecomp): Cannot open load file: No such file or directory, proof-autoloads
Error (bytecomp): Cannot open load file: No such file or directory, proof-utils
Error (bytecomp): Cannot open load file: No such file or directory, proof-splash
Error (bytecomp): Cannot open load file: No such file or directory, pg-pamacs
Error (bytecomp): Cannot open load file: No such file or directory, span [2 times]
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Error (bytecomp): Cannot open load file: No such file or directory, span
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, pg-xml
Error (bytecomp): Cannot open load file: No such file or directory, proof-utils
Error (bytecomp): Cannot open load file: No such file or directory, span
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, proof-utils
Error (bytecomp): Cannot open load file: No such file or directory, pg-vars
Error (bytecomp): Cannot open load file: No such file or directory, proof-utils
Error (bytecomp): Cannot open load file: No such file or directory, proof-useropts
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, span
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Error (bytecomp): Cannot open load file: No such file or directory, proof-config
Error (bytecomp): Cannot open load file: No such file or directory, proof-auxmodes
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, proof-utils
Error (bytecomp): Cannot open load file: No such file or directory, proof-auxmodes
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, span
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, span
Error (bytecomp): Cannot open load file: No such file or directory, pg-vars
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Error (bytecomp): Cannot open load file: No such file or directory, proof-config
Error (bytecomp): Cannot open load file: No such file or directory, span
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, proof-shell
Error (bytecomp): Cannot open load file: No such file or directory, scomint
Error (bytecomp): Cannot open load file: No such file or directory, proof-site [3 times]
Error (bytecomp): Cannot open load file: No such file or directory, proof-unicode-tokens
Error (bytecomp): Cannot open load file: No such file or directory, proof-easy-config [2 times]
Error (bytecomp): Cannot open load file: No such file or directory, span
Error (bytecomp): Cannot open load file: No such file or directory, pg-autotest
Error (bytecomp): Cannot open load file: No such file or directory, pg-vars
Error (bytecomp): Cannot open load file: No such file or directory, mmm-auto
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, proof-syntax
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, unicode-tokens
Error (bytecomp): Cannot open load file: No such file or directory, span
Error (bytecomp): Cannot open load file: No such file or directory, proof-syntax
Error (bytecomp): Cannot open load file: No such file or directory, proof
Error (bytecomp): Cannot open load file: No such file or directory, span
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Warning (bytecomp): cl package required at runtime [2 times]
Error (bytecomp): Cannot open load file: No such file or directory, maths-menu
Error (bytecomp): Cannot open load file: No such file or directory, proof-easy-config [3 times]
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, span
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, pg-pbrpm
Error (bytecomp): Cannot open load file: No such file or directory, proof-compat
Error (bytecomp): Cannot open load file: No such file or directory, proof
Warning (bytecomp): reference to free variable ‘*whitespace*’
Warning (bytecomp): reference to free variable ‘*twelf-comment-start*’
Warning (bytecomp): reference to free variable ‘*whitespace*’ [2 times]
Warning (bytecomp): reference to free variable ‘*twelf-id-chars*’
Warning (bytecomp): Use ‘with-current-buffer’ rather than save-excursion+set-buffer
Warning (bytecomp): assignment to free variable ‘*twelf-error-pos*’
Warning (bytecomp): the following functions are not known to be defined: font-lock-any-faces-p,
    font-lock-set-face
Warning (bytecomp): ‘goto-line’ is for interactive use only; use ‘forward-line’ instead. [3 times]
Warning (bytecomp): Use ‘with-current-buffer’ rather than save-excursion+set-buffer
Warning (bytecomp): file-name-directory called with 2 arguments, but accepts only 1
Warning (bytecomp): Use ‘with-current-buffer’ rather than save-excursion+set-buffer [10 times]
Warning (bytecomp): assignment to free variable ‘comint-match-partial-pathname-chars’
Warning (bytecomp): Use ‘with-current-buffer’ rather than save-excursion+set-buffer
Warning (bytecomp): !! The file uses old-style backquotes !!
This functionality has been obsolete for more than 10 years already
and will be removed soon.  See (elisp)Backquote in the manual. [2 times]
Warning (bytecomp): the following functions are not known to be defined: toggle, radio
Error (bytecomp): Cannot open load file: No such file or directory, proof-easy-config
Warning (bytecomp): reference to free variable ‘proof-home-directory’
Warning (bytecomp): the following functions are not known to be defined: ml4pg-init-clusters,
    ml4pg-activate-icons, ml4pg-exported-libraries,
    ml4pg-extract-theorems-library, proof-shell-invisible-cmd-get-result
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-vars
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-vars
Error (bytecomp): Cannot open load file: No such file or directory, mmm-compat
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-compat [2 times]
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-compat
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-compat
Error (bytecomp): Cannot open load file: No such file or directory, mmm-auto [3 times]
Warning (bytecomp): cl package required at runtime
Error (bytecomp): Cannot open load file: No such file or directory, mmm-compat
Warning (bytecomp): global/dynamic var ‘vis’ lacks a prefix
Warning (bytecomp): assignment to free variable ‘proof-nested-goals-p’
Warning (bytecomp): reference to free variable ‘isar-goal-command-regexp’
Warning (bytecomp): reference to free variable ‘isar-local-goal-command-regexp’
Warning (bytecomp): assignment to free variable ‘proof-goal-command-regexp’
Warning (bytecomp): reference to free variable ‘proof-goal-command-regexp’
Warning (bytecomp): assignment to free variable ‘proof-really-save-command-p’
Warning (bytecomp): assignment to free variable ‘proof-script-use-old-parser’
Warning (bytecomp): reference to free variable ‘isar-keywords-major’
Warning (bytecomp): assignment to free variable ‘isar-any-command-regexp’
Warning (bytecomp): the following functions are not known to be defined: proof-string-match,
    isar-ids-to-regexp
Warning (bytecomp): the following functions are not known to be defined: pg-clear-test-suite,
    pg-set-test-suite, pg-test-eval, pg-pgip-interpret-value
Warning (bytecomp): Use ‘with-current-buffer’ rather than save-excursion+set-buffer
Warning (bytecomp): the function ‘remassoc’ is not known to be defined.
Error (bytecomp): Cannot open load file: No such file or directory, proof-site
Error (bytecomp): Cannot open load file: No such file or directory, proof [2 times]
Error (bytecomp): Cannot open load file: No such file or directory, proof-syntax
Error (bytecomp): Cannot open load file: No such file or directory, proof
Warning (bytecomp): function ‘remove-if-not’ from cl package called at runtime [3 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-goal-level’
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-tactic’
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): assignment to free variable ‘goal-level-temp’
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘goal-level-temp’
Warning (bytecomp): assignment to free variable ‘goal-level-temp’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [7 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [6 times]
Warning (bytecomp): reference to free variable ‘proof-tree-level’
Warning (bytecomp): reference to free variable ‘tactic-level’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [6 times]
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): the following functions are not known to be defined: ml4pg-read-lemmas,
    proof-shell-invisible-cmd-get-result, proof-undo-last-successful-command,
    proof-assert-next-command-interactive, ml4pg-save-lemma, get-obj-intro,
    proof-queue-or-locked-end, proof-segment-up-to-using-cache,
    proof-goto-point
Warning (bytecomp): reference to free variable ‘*matlab-program*’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘times’
Warning (bytecomp): assignment to free variable ‘times’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): reference to free variable ‘times’
Warning (bytecomp): assignment to free variable ‘times’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): assignment to free variable ‘res’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘res’
Warning (bytecomp): reference to free variable ‘tactic-temp’
Warning (bytecomp): reference to free variable ‘tactic-level’
Warning (bytecomp): reference to free variable ‘proof-tree-temp’
Warning (bytecomp): reference to free variable ‘proof-tree-level’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-ml-system’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-frequency-precision’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-frequency-precision’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘tactic-level’
Warning (bytecomp): reference to free variable ‘proof-tree-level’
Warning (bytecomp): reference to free variable ‘ml4pg-ml-system’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems2’ [2 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-saved-theorems2’
Warning (bytecomp): the following functions are not known to be defined: ml4pg-remove-jumps,
    read-lines, ml4pg-read-lines, ml4pg-extract-clusters-from-file,
    ml4pg-clusters-of-n, ml4pg-unzip, ml4pg-quicksort-pair, ml4pg-zip,
    ml4pg-remove-alone, ml4pg-form-clusters, ml4pg-extract-info-up-to-here,
    ml4pg-extract-features-1-bis, ml4pg-extract-features-2-bis, ml4pg-weka,
    proof-shell-invisible-cmd-get-result, ml4pg-extract-features-1,
    ml4pg-extract-features-2, ml4pg-print-clusters-matlab, ml4pg-left-strings,
    ml4pg-extract-names-dynamic, ml4pg-assign-values,
    ml4pg-complete-names-values, ml4pg-recompute-saved-theorems,
    ml4pg-extract-features-dynamic
Warning (bytecomp): reference to free variable ‘coq-mode-map’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-libs’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): assignment to free variable ‘libs-menus’
Warning (bytecomp): the function ‘string-member’ is not known to be defined.
Warning (bytecomp): reference to free variable ‘ml4pg-save-automatically’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘temp’
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): assignment to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): ‘end-of-buffer’ is for interactive use only; use ‘(goto-char (point-max))’ instead.
Warning (bytecomp): reference to free variable ‘ml4pg-dirs’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): the following functions are not known to be defined:
    proof-assert-next-command-interactive, proof-goto-point,
    proof-queue-or-locked-end, proof-segment-up-to-using-cache,
    ml4pg-get-top-symbol, ml4pg-get-number-of-goals, get-number-of-goals,
    get-numbers, get-name, ml4pg-flat, ml4pg-extract-feature-theorems,
    ml4pg-string-member, ml4pg-extract-features-1, ml4pg-extract-names
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’ [3 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-theorems_id’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): assignment to free variable ‘ml4pg-views_id’
Warning (bytecomp): function ‘search’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): the function ‘sml4pg-ave-view-aux’ is not known to be defined.
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘*weka-dir*’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘remove-if-not’ from cl package called at runtime [3 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-goal-level’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [4 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [6 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [13 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [4 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [8 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [29 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [9 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [7 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [5 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng’
Warning (bytecomp): reference to free variable ‘tactic-level’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): the following functions are not known to be defined: ml4pg-read-lemmas,
    ml4pg-read-views, proof-shell-invisible-cmd-get-result,
    proof-undo-last-successful-command, proof-assert-next-command-interactive,
    ml4pg-save-view, ml4pg-save-lemma, cml4pg-ompute-value-simpl,
    proof-queue-or-locked-end, proof-segment-up-to-using-cache,
    ml4pg-remove_last_colon, proof-goto-point, find-max-length
Warning (bytecomp): reference to free variable ‘*matlab-program*’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘granularity-level-temp’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’ [2 times]
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp-res’
Warning (bytecomp): reference to free variable ‘temp-res’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): assignment to free variable ‘signal’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-iterative’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): assignment to free variable ‘res’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘res’
Warning (bytecomp): reference to free variable ‘ml4pg-tactic-temp’
Warning (bytecomp): reference to free variable ‘ml4pg-tactic-level’
Warning (bytecomp): reference to free variable ‘ml4pg-proof-tree-temp’
Warning (bytecomp): reference to free variable ‘ml4pg-proof-tree-level’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-ml-system’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-frequency-precision’
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-frequency-precision’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-tactic-level’
Warning (bytecomp): reference to free variable ‘ml4pg-proof-tree-level’
Warning (bytecomp): reference to free variable ‘ml4pg-ml-system’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-level’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-libs-menus’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems2’ [2 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-saved-theorems2’
Warning (bytecomp): the following functions are not known to be defined: ml4pg-remove-jumps,
    ml4pg-read-lines, ml4pg-extract-clusters-from-file, ml4pg-clusters-of-n,
    ml4pg-unzip, ml4pg-quicksort-pair, ml4pg-zip, read-lines,
    ml4pg-remove-alone, ml4pg-form-clusters, ml4pg-extract-info-up-to-here,
    ml4pg-extract-features-1-bis, ml4pg-extract-features-2-bis, ml4pg-weka,
    proof-shell-invisible-cmd-get-result, ml4pg-extract-features-1,
    ml4pg-extract-features-2, ml4pg-left-strings, ml4pg-extract-names-dynamic,
    ml4pg-assign-values, ml4pg-complete-names-values,
    ml4pg-recompute-saved-theorems, ml4pg-extract-features-dynamic
Warning (bytecomp): reference to free variable ‘coq-mode-map’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘granularity-level’
Warning (bytecomp): reference to free variable ‘ml4pg-libs’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead. [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘ml4pg-save-automatically’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): assignment to free variable ‘temp’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): reference to free variable ‘temp’
Warning (bytecomp): assignment to free variable ‘ng’
Warning (bytecomp): assignment to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ng2’
Warning (bytecomp): reference to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): assignment to free variable ‘ml4pg-saved-theorems’
Warning (bytecomp): ‘beginning-of-buffer’ is for interactive use only; use ‘(goto-char (point-min))’ instead.
Warning (bytecomp): ‘end-of-buffer’ is for interactive use only; use ‘(goto-char (point-max))’ instead.
Warning (bytecomp): reference to free variable ‘ml4pg-dirs’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime
Warning (bytecomp): the following functions are not known to be defined:
    proof-assert-next-command-interactive, proof-goto-point,
    proof-queue-or-locked-end, proof-segment-up-to-using-cache,
    ml4pg-get-top-symbol, ml4pg-get-number-of-goals, ml4pg-get-numbers, flat,
    ml4pg-extract-feature-theorems, ml4pg-string-member,
    ml4pg-extract-features-1, ml4pg-extract-names
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’ [3 times]
Warning (bytecomp): assignment to free variable ‘ml4pg-theorems_id’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): assignment to free variable ‘ml4pg-views_id’
Warning (bytecomp): function ‘search’ from cl package called at runtime [3 times]
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [3 times]
Warning (bytecomp): reference to free variable ‘ml4pg-algorithm’
Warning (bytecomp): reference to free variable ‘ml4pg-home-dir’
Warning (bytecomp): reference to free variable ‘*weka-dir*’
Warning (bytecomp): assignment to free variable ‘foo’
Warning (bytecomp): reference to free variable ‘foo’
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime [2 times]
Warning (bytecomp): function ‘search’ from cl package called at runtime
Warning (bytecomp): function ‘subseq’ from cl package called at runtime