This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to branch master
in repository hol-light.

      from  e4242ac   quick fix for building with camlp5 7.01
       new  64d942d   New upstream version 20170917
       new  7b77dc8   Merge tag 'upstream/20170917'
       new  c1db1ae   new upstream version 20170917 and related changes
       new  5c800a2   New upstream version 20171023
       new  7a6a8aa   Merge tag 'upstream/20171023'
       new  1c4af31   finish packaging with using various upstream fixes

The 6 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 100/circle.ml                                      |     6 +-
 100/inclusion_exclusion.ml                         |     2 +-
 100/lagrange.ml                                    |     1 +
 100/liouville.ml                                   |    26 -
 100/minkowski.ml                                   |   102 +-
 100/pnt.ml                                         |    24 +-
 100/sqrt.ml                                        |     1 -
 Boyer_Moore/README                                 |    18 +-
 Boyer_Moore/counterexample.ml                      |     2 +-
 Boyer_Moore/definitions.ml                         |     2 +-
 Boyer_Moore/environment.ml                         |     4 +-
 Boyer_Moore/equalities.ml                          |    11 +-
 Boyer_Moore/generalize.ml                          |    55 +-
 Boyer_Moore/induction.ml                           |     4 +-
 Boyer_Moore/irrelevance.ml                         |     7 +-
 Boyer_Moore/main.ml                                |   152 +-
 Boyer_Moore/make.ml                                |     8 +-
 Boyer_Moore/shells.ml                              |    14 +-
 Boyer_Moore/terms_and_clauses.ml                   |    22 +-
 Boyer_Moore/waterfall.ml                           |   140 +-
 CHANGES                                            |  1248 +-
 Complex/complex_grobner.ml                         |     6 +-
 Complex/complexnumbers.ml                          |     4 +-
 Complex/quelim.ml                                  |     4 +-
 Examples/borsuk.ml                                 |     2 +-
 Examples/division_algebras.ml                      |   196 +-
 Examples/kb.ml                                     |     2 +-
 Examples/machin.ml                                 |     2 +-
 Examples/pell.ml                                   |     2 +-
 Examples/prover9.ml                                |     4 +-
 Examples/sos.ml                                    |     2 +-
 Formal_ineqs/README.md                             |    18 +
 Formal_ineqs/README.txt                            |     8 -
 Formal_ineqs/arith/arith_cache.hl                  |    74 +-
 Formal_ineqs/arith/{float.hl => arith_float.hl}    |  8075 +++++-----
 Formal_ineqs/arith/arith_nat.hl                    |   106 +
 Formal_ineqs/arith/arith_num.hl                    |   552 +-
 Formal_ineqs/arith/eval_interval.hl                |   201 +-
 Formal_ineqs/arith/float_atn.hl                    |   582 -
 Formal_ineqs/arith/float_pow.hl                    |   526 +
 Formal_ineqs/arith/float_theory.hl                 |   206 +-
 Formal_ineqs/arith/interval_arith.hl               |   127 +-
 Formal_ineqs/arith/more_float.hl                   |  1087 +-
 Formal_ineqs/arith/nat.hl                          |   102 -
 Formal_ineqs/arith/num_exp_theory.hl               |   502 +-
 Formal_ineqs/arith_options.hl                      |    53 +-
 Formal_ineqs/docs/FormalVerifier.pdf               |   Bin 223139 -> 203253 
bytes
 Formal_ineqs/docs/FormalVerifier.tex               |    47 +-
 Formal_ineqs/examples.hl                           |    19 +-
 Formal_ineqs/examples_flyspeck.hl                  |   122 +-
 Formal_ineqs/examples_other.hl                     |    35 +
 Formal_ineqs/examples_poly.hl                      |    16 +-
 Formal_ineqs/informal/informal_arith.hl            |   805 -
 Formal_ineqs/informal/informal_asn_acs.hl          |   169 +
 Formal_ineqs/informal/informal_atn.hl              |   228 +
 Formal_ineqs/informal/informal_eval_interval.hl    |   208 +-
 Formal_ineqs/informal/informal_exp.hl              |   241 +
 Formal_ineqs/informal/informal_float.hl            |   526 +
 Formal_ineqs/informal/informal_interval.hl         |   248 +
 Formal_ineqs/informal/informal_log.hl              |   123 +
 Formal_ineqs/informal/informal_m_taylor.hl         |   403 -
 Formal_ineqs/informal/informal_m_verifier.hl       |   302 -
 Formal_ineqs/informal/informal_matan.hl            |   206 +
 Formal_ineqs/informal/informal_nat.hl              |   167 +
 Formal_ineqs/informal/informal_poly.hl             |   102 +
 Formal_ineqs/informal/informal_search.hl           |   298 +
 Formal_ineqs/informal/informal_sin_cos.hl          |   412 +
 Formal_ineqs/informal/informal_taylor.hl           |   667 +
 Formal_ineqs/informal/informal_verifier.hl         |   332 +
 .../jordan/parse_ext_override_interface.hl         |   213 -
 Formal_ineqs/jordan/real_ext.hl                    |   303 -
 Formal_ineqs/jordan/refinement.hl                  |    79 -
 Formal_ineqs/jordan/taylor_atn.hl                  |   917 --
 Formal_ineqs/lib/ipow.hl                           |   447 +
 Formal_ineqs/lib/ssrbool-compiled.hl               |   759 -
 Formal_ineqs/lib/ssrbool.hl                        |   767 +
 Formal_ineqs/lib/ssreflect/sections.hl             |   264 +-
 Formal_ineqs/lib/ssreflect/ssreflect.hl            |   611 +-
 Formal_ineqs/lib/ssrfun-compiled.hl                |   304 -
 Formal_ineqs/lib/ssrfun.hl                         |   375 +
 Formal_ineqs/lib/ssrnat-compiled.hl                |  1634 --
 Formal_ineqs/lib/ssrnat.hl                         |  2222 +++
 Formal_ineqs/list/list_conversions.hl              |   180 +-
 Formal_ineqs/list/list_float.hl                    |   404 +-
 Formal_ineqs/list/more_list.hl                     |   262 +-
 Formal_ineqs/make.ml                               |    48 -
 Formal_ineqs/misc/{misc.hl => misc_functions.hl}   |   143 +-
 Formal_ineqs/misc/{vars.hl => misc_vars.hl}        |   300 +-
 .../interval_m/report.ml => misc/report.hl}        |    26 +-
 Formal_ineqs/taylor/m_taylor.hl                    |  2978 ++--
 Formal_ineqs/taylor/m_taylor_arith.hl              |  2837 +++-
 Formal_ineqs/taylor/m_taylor_arith2.hl             |   897 +-
 .../taylor/theory/multivariate_taylor-compiled.hl  |  3967 ++---
 Formal_ineqs/taylor/theory/multivariate_taylor.vhl |  1119 +-
 .../taylor/theory/taylor_interval-compiled.hl      |  4113 +++--
 Formal_ineqs/taylor/theory/taylor_interval.vhl     |  1542 +-
 Formal_ineqs/tests/data/gen_nat_data.py            |    27 +
 Formal_ineqs/tests/float_data.hl                   |    40 +
 Formal_ineqs/tests/log.hl                          |    76 +
 Formal_ineqs/tests/nat_test.hl                     |   200 +
 Formal_ineqs/tests/results.hl                      |   109 +
 Formal_ineqs/tests/test_utils.hl                   |   185 +
 Formal_ineqs/trig/asn_acs_eval.hl                  |   413 +
 Formal_ineqs/trig/atn.hl                           |   309 +
 Formal_ineqs/trig/atn_eval.hl                      |   472 +
 Formal_ineqs/trig/cos_bounds_eval.hl               |   196 +
 Formal_ineqs/trig/cos_eval.hl                      |  1238 ++
 Formal_ineqs/trig/exp_eval.hl                      |   414 +
 Formal_ineqs/trig/exp_log.hl                       |   313 +
 Formal_ineqs/trig/log_eval.hl                      |   205 +
 Formal_ineqs/trig/matan.hl                         |   712 +
 Formal_ineqs/trig/matan_eval.hl                    |   379 +
 Formal_ineqs/trig/poly.hl                          |   231 +
 Formal_ineqs/trig/poly_eval.hl                     |   372 +
 Formal_ineqs/trig/series.hl                        |  1298 ++
 Formal_ineqs/trig/sin_cos.hl                       |   298 +
 Formal_ineqs/trig/sin_eval.hl                      |    87 +
 Formal_ineqs/trig/test.hl                          |    89 +
 Formal_ineqs/trig/unused.hl                        |   240 +
 Formal_ineqs/verifier/certificate.hl               |   284 +
 Formal_ineqs/verifier/interval_m/interval.ml       |   173 -
 Formal_ineqs/verifier/interval_m/line_interval.ml  |   114 -
 Formal_ineqs/verifier/interval_m/recurse.ml        |   315 -
 Formal_ineqs/verifier/interval_m/recurse0.ml       |   152 -
 Formal_ineqs/verifier/interval_m/taylor.ml         |   376 -
 Formal_ineqs/verifier/interval_m/types.ml          |    52 -
 Formal_ineqs/verifier/interval_m/univariate.ml     |   107 -
 Formal_ineqs/verifier/interval_m/verifier.ml       |   305 -
 Formal_ineqs/verifier/m_verifier.hl                |  1466 +-
 Formal_ineqs/verifier/m_verifier_build.hl          |   193 +-
 Formal_ineqs/verifier/m_verifier_main.hl           |   731 +-
 Formal_ineqs/verifier_options.hl                   |    36 +-
 Functionspaces/cfunspace.ml                        |    89 +-
 Help/HYP_TAC.doc                                   |     0
 IEEE/fixed_thms.hl                                 |     2 +-
 IsabelleLight/README                               |    71 +-
 IsabelleLight/meta_rules.ml                        |   174 +-
 IsabelleLight/new_tactics.ml                       |   255 +-
 IsabelleLight/support.ml                           |   149 +-
 Jordan/jordan_curve_theorem.ml                     |    61 +-
 Jordan/metric_spaces.ml                            |    17 +-
 Jordan/num_ext_nabs.ml                             |     2 +-
 Jordan/real_ext.ml                                 |     2 +-
 Jordan/tactics_ext2.ml                             |    10 +-
 Library/analysis.ml                                |    88 +-
 Library/card.ml                                    |   601 +-
 Library/floor.ml                                   |   105 +-
 Library/frag.ml                                    |   418 +
 Library/grouptheory.ml                             |  4442 ++++++
 Library/pocklington.ml                             |    10 +-
 Library/pratt.ml                                   |     4 +-
 Library/prime.ml                                   |    63 +-
 Library/transc.ml                                  |   233 +-
 Makefile                                           |    19 +-
 Minisat/minisat_parse.ml                           |    10 +-
 Multivariate/canal.ml                              |    30 +-
 Multivariate/cauchy.ml                             |    28 +-
 Multivariate/complex_database.ml                   |  1360 +-
 Multivariate/complexes.ml                          |    16 +-
 Multivariate/convex.ml                             |    51 +-
 Multivariate/cvectors.ml                           |    11 +-
 Multivariate/degree.ml                             |   314 +-
 Multivariate/derivatives.ml                        |    26 +-
 Multivariate/determinants.ml                       |   186 +-
 Multivariate/flyspeck.ml                           |    85 +-
 Multivariate/geom.ml                               |    24 +-
 Multivariate/homology.ml                           |  3776 +++++
 Multivariate/integration.ml                        |   148 +-
 Multivariate/lpspaces.ml                           |   107 +-
 Multivariate/measure.ml                            |   252 +-
 Multivariate/metric.ml                             | 15025 ++++++++++++++++++-
 Multivariate/misc.ml                               |   949 +-
 Multivariate/moretop.ml                            |   214 +-
 Multivariate/multivariate_database.ml              |  1344 +-
 Multivariate/paths.ml                              |   983 +-
 Multivariate/polytope.ml                           |    32 +-
 Multivariate/realanalysis.ml                       |  2358 ++-
 Multivariate/topology.ml                           |  5901 +++++---
 Multivariate/transcendentals.ml                    |   134 +-
 Multivariate/vectors.ml                            |   564 +-
 Ntrie/ntrie.ml                                     |  1377 +-
 Ntrie/ntrie_tests.ml                               |   181 -
 Proofrecording/hol_light/Makefile                  |    74 +-
 Proofrecording/tools/detecteq.jar                  |   Bin 7516 -> 0 bytes
 Proofrecording/tools/nametheorems.jar              |   Bin 2482 -> 0 bytes
 Proofrecording/tools/src/Makefile                  |    13 +
 Quaternions/qanal.hl                               |     4 +-
 Quaternions/qnormalizer.hl                         |    21 +-
 .../TarskiAxiomGeometry_read.ml                    |     0
 Rqe/asym.ml                                        |     4 +-
 Rqe/inferisign_thms.ml                             |     2 +-
 Rqe/inferpsign_thms.ml                             |     2 +-
 Tutorial/Custom_inference_rules.ml                 |     2 +-
 Tutorial/all.ml                                    |     2 +-
 arith.ml                                           |    28 +
 calc_int.ml                                        |     2 +-
 calc_rat.ml                                        |    62 +-
 cart.ml                                            |    33 +-
 class.ml                                           |     2 +-
 database.ml                                        |   197 +-
 debian/README.Debian                               |    25 +-
 debian/changelog                                   |    20 +-
 debian/compat                                      |     2 +-
 debian/control                                     |    15 +-
 debian/copyright                                   |    47 +-
 debian/hol-light-source.exclude                    |     1 +
 debian/patches/camlp5-7.patch                      |    23 -
 debian/patches/holtest-no-proof-recording.patch    |     2 +-
 debian/patches/series                              |     1 -
 debian/rules                                       |     7 +-
 drule.ml                                           |     4 +-
 grobner.ml                                         |    10 +-
 holtest                                            |     3 +
 holtest.mk                                         |   100 +-
 ind_types.ml                                       |     4 +-
 int.ml                                             |    54 +-
 lists.ml                                           |    39 +-
 nums.ml                                            |     8 +-
 pa_j_3.1x_6.11.ml => pa_j_4.xx_7.xx.ml             |     5 +-
 pair.ml                                            |    27 +-
 parser.ml                                          |    34 +-
 printer.ml                                         |    41 +-
 real.ml                                            |   477 +-
 sets.ml                                            |   900 +-
 tactics.ml                                         |     2 +-
 225 files changed, 76396 insertions(+), 28090 deletions(-)
 create mode 100644 Formal_ineqs/README.md
 delete mode 100644 Formal_ineqs/README.txt
 rename Formal_ineqs/arith/{float.hl => arith_float.hl} (61%)
 create mode 100644 Formal_ineqs/arith/arith_nat.hl
 delete mode 100644 Formal_ineqs/arith/float_atn.hl
 create mode 100644 Formal_ineqs/arith/float_pow.hl
 delete mode 100644 Formal_ineqs/arith/nat.hl
 create mode 100644 Formal_ineqs/examples_other.hl
 delete mode 100644 Formal_ineqs/informal/informal_arith.hl
 create mode 100644 Formal_ineqs/informal/informal_asn_acs.hl
 create mode 100644 Formal_ineqs/informal/informal_atn.hl
 create mode 100644 Formal_ineqs/informal/informal_exp.hl
 create mode 100644 Formal_ineqs/informal/informal_float.hl
 create mode 100644 Formal_ineqs/informal/informal_interval.hl
 create mode 100644 Formal_ineqs/informal/informal_log.hl
 delete mode 100644 Formal_ineqs/informal/informal_m_taylor.hl
 delete mode 100644 Formal_ineqs/informal/informal_m_verifier.hl
 create mode 100644 Formal_ineqs/informal/informal_matan.hl
 create mode 100644 Formal_ineqs/informal/informal_nat.hl
 create mode 100644 Formal_ineqs/informal/informal_poly.hl
 create mode 100644 Formal_ineqs/informal/informal_search.hl
 create mode 100644 Formal_ineqs/informal/informal_sin_cos.hl
 create mode 100644 Formal_ineqs/informal/informal_taylor.hl
 create mode 100644 Formal_ineqs/informal/informal_verifier.hl
 delete mode 100644 Formal_ineqs/jordan/parse_ext_override_interface.hl
 delete mode 100644 Formal_ineqs/jordan/real_ext.hl
 delete mode 100644 Formal_ineqs/jordan/refinement.hl
 delete mode 100644 Formal_ineqs/jordan/taylor_atn.hl
 create mode 100644 Formal_ineqs/lib/ipow.hl
 delete mode 100644 Formal_ineqs/lib/ssrbool-compiled.hl
 create mode 100644 Formal_ineqs/lib/ssrbool.hl
 delete mode 100644 Formal_ineqs/lib/ssrfun-compiled.hl
 create mode 100644 Formal_ineqs/lib/ssrfun.hl
 delete mode 100644 Formal_ineqs/lib/ssrnat-compiled.hl
 create mode 100644 Formal_ineqs/lib/ssrnat.hl
 rename Formal_ineqs/misc/{misc.hl => misc_functions.hl} (51%)
 rename Formal_ineqs/misc/{vars.hl => misc_vars.hl} (54%)
 rename Formal_ineqs/{verifier/interval_m/report.ml => misc/report.hl} (73%)
 create mode 100755 Formal_ineqs/tests/data/gen_nat_data.py
 create mode 100644 Formal_ineqs/tests/float_data.hl
 create mode 100644 Formal_ineqs/tests/log.hl
 create mode 100644 Formal_ineqs/tests/nat_test.hl
 create mode 100644 Formal_ineqs/tests/results.hl
 create mode 100644 Formal_ineqs/tests/test_utils.hl
 create mode 100644 Formal_ineqs/trig/asn_acs_eval.hl
 create mode 100644 Formal_ineqs/trig/atn.hl
 create mode 100644 Formal_ineqs/trig/atn_eval.hl
 create mode 100644 Formal_ineqs/trig/cos_bounds_eval.hl
 create mode 100644 Formal_ineqs/trig/cos_eval.hl
 create mode 100644 Formal_ineqs/trig/exp_eval.hl
 create mode 100644 Formal_ineqs/trig/exp_log.hl
 create mode 100644 Formal_ineqs/trig/log_eval.hl
 create mode 100644 Formal_ineqs/trig/matan.hl
 create mode 100644 Formal_ineqs/trig/matan_eval.hl
 create mode 100644 Formal_ineqs/trig/poly.hl
 create mode 100644 Formal_ineqs/trig/poly_eval.hl
 create mode 100644 Formal_ineqs/trig/series.hl
 create mode 100644 Formal_ineqs/trig/sin_cos.hl
 create mode 100644 Formal_ineqs/trig/sin_eval.hl
 create mode 100644 Formal_ineqs/trig/test.hl
 create mode 100644 Formal_ineqs/trig/unused.hl
 create mode 100644 Formal_ineqs/verifier/certificate.hl
 delete mode 100644 Formal_ineqs/verifier/interval_m/interval.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/line_interval.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/recurse.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/recurse0.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/taylor.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/types.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/univariate.ml
 delete mode 100644 Formal_ineqs/verifier/interval_m/verifier.ml
 mode change 100755 => 100644 Help/HYP_TAC.doc
 create mode 100644 Library/frag.ml
 create mode 100644 Library/grouptheory.ml
 mode change 100755 => 100644 Multivariate/cvectors.ml
 create mode 100644 Multivariate/homology.ml
 delete mode 100644 Ntrie/ntrie_tests.ml
 delete mode 100644 Proofrecording/tools/detecteq.jar
 delete mode 100644 Proofrecording/tools/nametheorems.jar
 create mode 100644 Proofrecording/tools/src/Makefile
 mode change 100755 => 100644 
RichterHilbertAxiomGeometry/TarskiAxiomGeometry_read.ml
 delete mode 100644 debian/patches/camlp5-7.patch
 copy pa_j_3.1x_6.11.ml => pa_j_4.xx_7.xx.ml (99%)
 mode change 100644 => 100755

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git

_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

Reply via email to