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

treinen pushed a commit to branch try
in repository why.

commit 8c0349f3018140d9f6e503cda5df56586ea008df
Merge: e74847a e2becea
Author: Ralf Treinen <trei...@free.fr>
Date:   Tue Mar 15 20:52:33 2016 +0100

    Merge tag 'upstream/2.35'
    
    Upstream version 2.35

 .depend                                            |  580 ++--
 CHANGES                                            |   13 +-
 Makefile.in                                        |   71 +-
 Version                                            |    6 +-
 configure                                          |  334 +-
 configure.in                                       |  216 +-
 doc/Makefile                                       |    4 +-
 frama-c-plugin/Makefile                            |   11 +-
 frama-c-plugin/common.ml                           |   19 +-
 frama-c-plugin/common.mli                          |    6 +
 frama-c-plugin/interp.ml                           |   14 +
 frama-c-plugin/jessie_config.ml                    |   31 -
 frama-c-plugin/jessie_options.ml                   |   12 +-
 frama-c-plugin/ptests_local_config.ml              |   37 -
 frama-c-plugin/register.ml                         |    2 +-
 frama-c-plugin/rewrite.ml                          |   39 +-
 intf/astnprinter.ml                                |    1 -
 intf/astpprinter.ml                                |    1 -
 intf/astprinter.ml                                 |    4 +-
 intf/cache.ml                                      |    2 -
 intf/model.ml                                      |    8 +-
 intf/pprinter.ml                                   |  205 +-
 intf/stat.ml                                       |    5 -
 intf/tagsplit.mll                                  |    2 -
 java/java_abstract.ml                              |    2 +-
 java/java_analysis.ml                              |    2 +-
 java/java_interp.ml                                |    5 +-
 java/java_main.ml                                  |    1 -
 java/java_options.ml                               |    6 +-
 java/java_parser.mly                               |    1 -
 java/java_typing.ml                                |   11 +-
 jc/jc_ai.mli                                       |    1 -
 jc/jc_annot_fail.ml                                |    2 +
 jc/jc_ast.mli                                      |    2 -
 jc/jc_callgraph.ml                                 |    3 +-
 jc/jc_constructors.ml                              |   29 +-
 jc/jc_effect.ml                                    |    2 +-
 jc/jc_envset.ml                                    |    2 +
 jc/jc_frame.ml                                     |  666 ++--
 jc/jc_frame_notin.ml                               |    6 -
 jc/jc_interp.ml                                    |    8 +-
 jc/jc_interp_misc.ml                               |   22 +-
 jc/jc_invariants.ml                                |    2 +-
 jc/jc_iterators.ml                                 |   10 +-
 jc/jc_iterators.mli                                |    2 +
 jc/jc_lexer.mll                                    |    4 +
 jc/jc_main.ml                                      |    1 -
 jc/jc_make.ml                                      |    4 +-
 jc/jc_name.ml                                      |    3 +-
 jc/jc_norm.ml                                      |    7 +-
 jc/jc_norm.mli                                     |    2 -
 jc/jc_options.ml                                   |    8 +-
 jc/jc_parser.mly                                   |    2 -
 jc/jc_pervasives.ml                                |   19 +-
 jc/jc_pervasives.mli                               |    2 +
 jc/jc_poutput.ml                                   |    3 -
 jc/jc_region.ml                                    |  134 +-
 jc/jc_separation.ml                                |    1 -
 jc/jc_stdlib_ge40.ml                               |  260 --
 jc/jc_typing.ml                                    |   10 +-
 jc/output.ml                                       |   35 +-
 lib/coq/WhyFloats.v                                |    7 +-
 lib/why3/coq.drv                                   |    4 +-
 lib/why3/{jessie3.mlw => jessie_why3.mlw}          |    2 +-
 ...integer.why => jessie_why3integer_obsolete.why} |    2 +
 ...jessie3theories.why => jessie_why3theories.why} |    0
 src/coq.ml                                         |    6 +-
 src/coq.mli                                        |    6 -
 src/cvcl.ml                                        |   26 +-
 src/cvcl.mli                                       |    7 -
 src/dispatcher.ml                                  |    3 +-
 src/effect.ml                                      |    4 +
 src/encoding.mli                                   |    2 -
 src/encoding_mono.ml                               |    2 +-
 src/encoding_mono_inst.ml                          |  280 +-
 src/encoding_pred.ml                               |   78 +-
 src/encoding_pred.mli                              |    5 -
 src/encoding_rec.ml                                |  124 +-
 src/encoding_rec.mli                               |    5 -
 src/encoding_strat.ml                              |   88 +-
 src/encoding_strat.mli                             |    5 -
 src/env.ml                                         |    6 +
 src/explain.ml                                     |    3 +-
 src/fastwp.ml                                      |    8 +-
 src/gappa.ml                                       |    9 +-
 src/gappa.mli                                      |    7 -
 src/harvey.ml                                      |    1 -
 src/harvey.mli                                     |    7 -
 src/hol4.ml                                        |    4 +-
 src/hol4.mli                                       |    7 -
 src/holl.ml                                        |    2 -
 src/holl.mli                                       |    7 -
 src/hypotheses_filtering.ml                        |    6 -
 src/isabelle.ml                                    |    8 +-
 src/isabelle.mli                                   |    4 -
 src/loc.ml                                         |    2 +
 src/misc.ml                                        |  157 +-
 src/misc.mli                                       |    1 -
 src/mizar.ml                                       |   38 +-
 src/mizar.mli                                      |    6 -
 src/mlize.mli                                      |    2 -
 src/monad.ml                                       |    5 +-
 src/monomorph.ml                                   |    9 +-
 src/ocaml.ml                                       |    2 +
 src/options.ml                                     |  334 +-
 src/parser.mly                                     |    3 +-
 src/predDefExpansor.ml                             |    3 +-
 src/pretty.ml                                      |    2 +
 src/project.ml                                     |    3 +-
 src/pvs.ml                                         |    5 +-
 src/pvs.mli                                        |    7 -
 src/red.ml                                         |    4 +-
 src/regen.ml                                       |    2 -
 src/regen.mli                                      |    1 -
 src/rename.ml                                      |    4 +-
 src/report.ml                                      |    7 +-
 src/simplify.ml                                    |  129 +-
 src/simplify.mli                                   |    6 -
 src/smtlib.ml                                      |   20 +-
 src/smtlib.mli                                     |    6 -
 src/theory_filtering.ml                            |    9 +-
 src/theoryreducer.ml                               |    8 -
 src/typing.ml                                      |   17 +-
 src/util.ml                                        |   24 +-
 src/util.mli                                       |    1 -
 src/vcg.ml                                         |   18 +-
 src/vcg.mli                                        |    1 -
 src/why3.ml                                        |    3 +-
 src/wp.ml                                          |    7 +
 src/z3.ml                                          |    8 +-
 src/z3.mli                                         |    6 -
 src/zenon.ml                                       |  118 +-
 src/zenon.mli                                      |    7 -
 tests/c/Sterbenz.jessie/coq/floats_strict_why.v    |  289 --
 tests/c/array_max.c                                |    2 +-
 tests/c/binary_search.c                            |    2 +-
 tests/c/{binary_search.c => binary_search_wrong.c} |    2 +-
 tests/c/duplets.c                                  |    6 +-
 tests/c/float_array.c                              |   12 +-
 tests/c/fresh.c                                    |   33 +
 tests/c/my_cosine.c                                |    2 +-
 tests/c/oracle/Sterbenz.res.oracle                 |   28 +-
 tests/c/oracle/array_double.res.oracle             |  188 +-
 tests/c/oracle/array_max.res.oracle                |  192 +-
 tests/c/oracle/binary_heap.res.oracle              |   26 +-
 tests/c/oracle/binary_search.res.oracle            |   26 +-
 tests/c/oracle/cd1d.res.oracle                     |  115 +-
 tests/c/oracle/clock_drift.res.oracle              |   28 +-
 tests/c/oracle/conjugate.res.oracle                |  241 +-
 .../double_rounding_multirounding_model.res.oracle |   68 +-
 .../oracle/double_rounding_strict_model.res.oracle |   68 +-
 tests/c/oracle/duplets.res.oracle                  |  599 ++--
 tests/c/oracle/eps_line1.res.oracle                |  232 +-
 tests/c/oracle/eps_line2.res.oracle                |  232 +-
 tests/c/oracle/exp.res.oracle                      |   93 +-
 tests/c/oracle/find_array.res.oracle               |  197 +-
 tests/c/oracle/flag.res.oracle                     |   26 +-
 tests/c/oracle/float_array.res.oracle              |  665 ++--
 tests/c/oracle/float_sqrt.res.oracle               |   26 +-
 tests/c/oracle/floats_bsearch.res.oracle           |   26 +-
 tests/c/oracle/heap_sort.res.oracle                |   26 +-
 tests/c/oracle/insertion_sort.res.oracle           |   26 +-
 tests/c/oracle/interval_arith.res.oracle           |  627 ++--
 tests/c/oracle/isqrt.res.oracle                    |   26 +-
 tests/c/oracle/isqrt2.res.oracle                   | 3545 +++++++++++++++++++-
 tests/c/oracle/maze.res.oracle                     |   22 +-
 tests/c/oracle/minmax.res.oracle                   |   26 +-
 tests/c/oracle/muller.res.oracle                   |   26 +-
 tests/c/oracle/my_cosine.res.oracle                |   52 +-
 tests/c/oracle/overflow_level.res.oracle           |   79 +-
 tests/c/oracle/popHeap.res.oracle                  |  555 +--
 tests/c/oracle/power.res.oracle                    |  169 +-
 tests/c/oracle/quick_sort.res.oracle               |   26 +-
 tests/c/oracle/rec.res.oracle                      |   26 +-
 tests/c/oracle/scalar_product.res.oracle           |  222 +-
 tests/c/oracle/selection_sort.res.oracle           |   26 +-
 tests/c/oracle/sparse_array.res.oracle             |   22 +-
 tests/c/oracle/sparse_array2.res.oracle            |   26 +-
 tests/c/oracle/sum_array.res.oracle                |  286 +-
 tests/c/oracle/swap.res.oracle                     |   26 +-
 tests/c/oracle/tree_max.res.oracle                 |  174 +-
 tests/c/popHeap.c                                  |    2 +-
 tests/c/power.c                                    |   24 +-
 tests/c/sum_array.c                                |    8 +-
 tests/java/BankingExample.java                     |   26 +
 tests/java/BinarySearch.java                       |    5 +-
 .../{BinarySearch.java => BinarySearchWrong.java}  |    2 +-
 tests/java/MyCosine.java                           |    1 +
 tests/java/oracle/AllZeros.res.oracle              |   26 +-
 tests/java/oracle/ArrayMax.res.oracle              |  237 +-
 tests/java/oracle/Arrays.res.oracle                |   26 +-
 tests/java/oracle/Assertion.res.oracle             |   67 +-
 tests/java/oracle/BinarySearch.res.oracle          |   26 +-
 tests/java/oracle/Bug_sort_exns.res.oracle         |   45 +-
 tests/java/oracle/Counter.res.oracle               |   26 +-
 tests/java/oracle/Creation.res.oracle              |   26 +-
 tests/java/oracle/Duplets.res.oracle               |  147 +-
 tests/java/oracle/Fact.res.oracle                  |  128 +-
 tests/java/oracle/Fibonacci.res.oracle             |   26 +-
 tests/java/oracle/FlagStatic.res.oracle            |   26 +-
 tests/java/oracle/Fresh.res.oracle                 |   82 +-
 tests/java/oracle/Fresh2.res.oracle                |  168 +-
 tests/java/oracle/Fresh3.res.oracle                |  160 +-
 tests/java/oracle/Gcd.res.oracle                   |   26 +-
 tests/java/oracle/Hello.res.oracle                 |   26 +-
 tests/java/oracle/Isqrt.res.oracle                 |   26 +-
 tests/java/oracle/Literals.res.oracle              |   26 +-
 tests/java/oracle/MacCarthy.res.oracle             |   26 +-
 tests/java/oracle/Muller.res.oracle                |   26 +-
 tests/java/oracle/MullerTheory.res.oracle          |   26 +-
 tests/java/oracle/MyCosine.res.oracle              |   26 +-
 tests/java/oracle/NameConflicts.res.oracle         |   26 +-
 tests/java/oracle/Negate.res.oracle                |   26 +-
 tests/java/oracle/Power.res.oracle                 |  238 +-
 tests/java/oracle/PreAndOld.res.oracle             |   26 +-
 tests/java/oracle/Purse.res.oracle                 |   26 +-
 tests/java/oracle/SelectionSort.res.oracle         |   26 +-
 tests/java/oracle/SideEffects.res.oracle           |   26 +-
 tests/java/oracle/SimpleAlloc.res.oracle           |   26 +-
 tests/java/oracle/SimpleApplet.res.oracle          |   26 +-
 tests/java/oracle/Sort.res.oracle                  |   26 +-
 tests/java/oracle/Sort2.res.oracle                 |   26 +-
 tests/java/oracle/Switch.res.oracle                |   26 +-
 tests/java/oracle/Termination.res.oracle           |   26 +-
 tests/java/oracle/TestNonNull.res.oracle           |   26 +-
 tests/java/oracle/TreeMax.res.oracle               |  144 +-
 tests/java/oracle/bts15964.res.oracle              |   34 +-
 tools/cvcl_split.mll                               |    3 +-
 tools/dp.ml                                        |   34 +-
 tools/ergo_split.mll                               |    3 +-
 tools/rv_split.mll                                 |    1 -
 tools/simplify_lexer.mll                           |    2 -
 tools/simplify_split.mll                           |    1 -
 tools/smtlib_split.mll                             |    1 -
 tools/toolstat_pars.mly                            |   29 +-
 tools/whystat.ml                                   |    1 -
 tools/zenon_split.mll                              |    1 -
 237 files changed, 10214 insertions(+), 6168 deletions(-)

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/why.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