[Pkg-ocaml-maint-commits] [hol-light] branch master updated (e4242ac -> 1c4af31)
Hendrik Tews
hendrik-guest at moszumanska.debian.org
Sun Oct 29 21:00:05 UTC 2017
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
More information about the Pkg-ocaml-maint-commits
mailing list