1. 15 May, 2018 18 commits
  2. 14 May, 2018 15 commits
    • Guillaume Melquiond's avatar
      Make tables a bit slimmer. · 3609e841
      Guillaume Melquiond authored
      3609e841
    • Guillaume Melquiond's avatar
      6ac57559
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
    • Guillaume Melquiond's avatar
      dc340a08
    • MARCHE Claude's avatar
      fix broken session · 444bf9b9
      MARCHE Claude authored
      444bf9b9
    • MARCHE Claude's avatar
      fix broken session · 75ab8189
      MARCHE Claude authored
      75ab8189
    • Jean-Christophe Filliâtre's avatar
    • Jean-Christophe Filliâtre's avatar
      mach.array.Array63 now uses a sequence as a model · 4898a45d
      Jean-Christophe Filliâtre authored
      instead of a function of type int->'a
      a coercion is declared from arrays to sequences, so that notation a[i]
      in the logic now refers to the sequence operation
      small caveat: you have to open module seq.Seq to be able to use this
      notation
      4898a45d
    • MARCHE Claude's avatar
      Merge branch 'new_ide' · 5cac408d
      MARCHE Claude authored
      # Conflicts:
      #	Makefile.in
      #	examples/WP_revisited/blocking_semantics5/why3session.xml
      #	examples/WP_revisited/wp2/why3session.xml
      #	examples/algo63/why3session.xml
      #	examples/algo64/why3session.xml
      #	examples/algo65/why3session.xml
      #	examples/all_distinct/why3session.xml
      #	examples/arm/why3session.xml
      #	examples/avl/association_list/why3session.xml
      #	examples/avl/avl/why3session.xml
      #	examples/avl/priority_queue/why3session.xml
      #	examples/avl/ral/why3session.xml
      #	examples/avl/sorted/why3session.xml
      #	examples/avl/tables/why3session.xml
      #	examples/bag/why3session.xml
      #	examples/balance/why3session.xml
      #	examples/bellman_ford/why3session.xml
      #	examples/bignum/why3session.xml
      #	examples/binary_search/why3session.xml
      #	examples/binary_sort/why3session.xml
      #	examples/binary_sqrt/why3session.xml
      #	examples/binomial_heap/why3session.xml
      #	examples/bitcount/why3session.xml
      #	examples/bitvector_examples/why3session.xml
      #	examples/bitwalker/why3session.xml
      #	examples/braun_trees/why3session.xml
      #	examples/bresenham/why3session.xml
      #	examples/bts/16_subst/why3shapes.gz
      #	examples/bubble_sort/why3session.xml
      #	examples/checking_a_large_routine/why3session.xml
      #	examples/coincidence_count/why3session.xml
      #	examples/coincidence_count_list/why3session.xml
      #	examples/conjugate/why3session.xml
      #	examples/counting_sort/why3session.xml
      #	examples/cubic_root/why3session.xml
      #	examples/cursor/why3session.xml
      #	examples/decrease1/why3session.xml
      #	examples/defunctionalization/why3session.xml
      #	examples/dfa_example/why3session.xml
      #	examples/dfs/why3session.xml
      #	examples/dijkstra/why3session.xml
      #	examples/division/why3session.xml
      #	examples/double_wp/compiler/why3session.xml
      #	examples/double_wp/logic/why3session.xml
      #	examples/double_wp/specs/why3session.xml
      #	examples/dyck/why3session.xml
      #	examples/edit_distance/why3session.xml
      #	examples/esterel/why3session.xml
      #	examples/euler002/why3session.xml
      #	examples/euler011/why3session.xml
      #	examples/fenwick/why3session.xml
      #	examples/fib_memo/why3session.xml
      #	examples/fibonacci/why3session.xml
      #	examples/find/why3session.xml
      #	examples/finger_trees/why3session.xml
      #	examples/flag/why3session.xml
      #	examples/flag2/why3session.xml
      #	examples/foveoos11_challenge1/why3session.xml
      #	examples/foveoos11_challenge3/why3session.xml
      #	examples/gcd/why3session.xml
      #	examples/gcd_bezout/why3session.xml
      #	examples/generate_all_trees/why3session.xml
      #	examples/hackers-delight/why3session.xml
      #	examples/hashtbl_impl/why3session.xml
      #	examples/in_progress/2wp_gen/base/why3session.xml
      #	examples/in_progress/2wp_gen/game/why3session.xml
      #	examples/in_progress/2wp_gen/game_fmla/why3session.xml
      #	examples/in_progress/2wp_gen/game_wp/why3session.xml
      #	examples/in_progress/2wp_gen/order/why3session.xml
      #	examples/in_progress/2wp_gen/transfinite/why3session.xml
      #	examples/in_progress/2wp_gen/transition/why3session.xml
      #	examples/in_progress/2wp_gen/zorn/why3session.xml
      #	examples/in_progress/koda_ruskey/why3session.xml
      #	examples/in_progress/mp/why3session.xml
      #	examples/insertion_sort/why3session.xml
      #	examples/insertion_sort_list/why3session.xml
      #	examples/insertion_sort_naive/why3session.xml
      #	examples/inverse_in_place/why3session.xml
      #	examples/isqrt/why3session.xml
      #	examples/isqrt_von_neumann/why3session.xml
      #	examples/kmp/why3session.xml
      #	examples/knuth_prime_numbers/why3session.xml
      #	examples/koda_ruskey/why3session.xml
      #	examples/largest_prime_factor/why3session.xml
      #	examples/lcp/why3session.xml
      #	examples/leftist_heap/why3session.xml
      #	examples/linear_probing/why3session.xml
      #	examples/linked_list_rev/why3session.xml
      #	examples/logic/hello_proof/why3session.xml
      #	examples/max_matrix/why3session.xml
      #	examples/maximum_subarray/why3session.xml
      #	examples/mccarthy/why3session.xml
      #	examples/mergesort_array/why3session.xml
      #	examples/mergesort_list/why3session.xml
      #	examples/mergesort_queue/why3session.xml
      #	examples/mjrty/why3session.xml
      #	examples/muller/why3session.xml
      #	examples/my_cosine/why3session.xml
      #	examples/optimal_replay/why3session.xml
      #	examples/patience/why3session.xml
      #	examples/pigeonhole/why3session.xml
      #	examples/power/why3session.xml
      #	examples/queens/why3session.xml
      #	examples/queens_bv/why3session.xml
      #	examples/quicksort/why3session.xml
      #	examples/random_access_list/why3session.xml
      #	examples/register_allocation/why3session.xml
      #	examples/relabel/why3session.xml
      #	examples/remove_duplicate/why3session.xml
      #	examples/remove_duplicate_hash/why3session.xml
      #	examples/residual/why3session.xml
      #	examples/rightmostbittrick/why3session.xml
      #	examples/ropes/why3session.xml
      #	examples/same_fringe/why3session.xml
      #	examples/schorr_waite/why3session.xml
      #	examples/schorr_waite_via_recursion/why3session.xml
      #	examples/selection_sort/why3session.xml
      #	examples/sf/why3session.xml
      #	examples/sieve/why3session.xml
      #	examples/skew_heaps/why3session.xml
      #	examples/snapshotable_trees/why3session.xml
      #	examples/stdlib/array/why3session.xml
      #	examples/stdlib/list/why3session.xml
      #	examples/sudoku/why3session.xml
      #	examples/sum_of_digits/why3session.xml
      #	examples/sumrange/why3session.xml
      #	examples/tests-provers/ieee_float/why3session.xml
      #	examples/there_and_back_again/why3session.xml
      #	examples/topological_sorting/why3session.xml
      #	examples/tortoise_and_hare/why3session.xml
      #	examples/tower_of_hanoi/why3session.xml
      #	examples/toy_compiler/why3session.xml
      #	examples/tree_height/why3session.xml
      #	examples/tree_of_array/why3session.xml
      #	examples/tree_of_list/why3session.xml
      #	examples/unraveling_a_card_trick/why3session.xml
      #	examples/use_api/mlw.ml
      #	examples/vacid_0_binary_heaps/proofs/why3session.xml
      #	examples/vacid_0_build_maze/why3session.xml
      #	examples/vacid_0_red_black_trees/why3session.xml
      #	examples/vacid_0_sparse_array/why3session.xml
      #	examples/verifythis_2015_dancing_links/why3session.xml
      #	examples/verifythis_2015_parallel_gcd/why3session.xml
      #	examples/verifythis_2015_relaxed_prefix/why3session.xml
      #	examples/verifythis_2016_matrix_multiplication/matrices/why3session.xml
      #	examples/verifythis_2016_matrix_multiplication/matrices_ring_simp/why3session.xml
      #	examples/verifythis_2016_matrix_multiplication/naive/why3session.xml
      #	examples/verifythis_2016_matrix_multiplication/strassen/why3session.xml
      #	examples/verifythis_2016_matrix_multiplication/sum_extended/why3session.xml
      #	examples/verifythis_2016_tree_traversal/why3session.xml
      #	examples/verifythis_PrefixSumRec/why3session.xml
      #	examples/verifythis_fm2012_LRS/why3session.xml
      #	examples/verifythis_fm2012_treedel/why3session.xml
      #	examples/vstte10_aqueue/why3session.xml
      #	examples/vstte10_inverting/why3session.xml
      #	examples/vstte10_max_sum/why3session.xml
      #	examples/vstte10_queens/why3session.xml
      #	examples/vstte10_search_list/why3session.xml
      #	examples/vstte12_bfs/why3session.xml
      #	examples/vstte12_combinators/why3session.xml
      #	examples/vstte12_ring_buffer/why3session.xml
      #	examples/vstte12_tree_reconstruction/why3session.xml
      #	examples/vstte12_two_way_sort/why3session.xml
      #	examples/warshall_algorithm/why3session.xml
      #	examples/zeros/why3session.xml
      #	src/core/pretty.ml
      #	src/transform/introduction.ml
      #	tests/theory-sessions/bintree/why3session.xml
      #	tests/theory-sessions/hashtbl/why3session.xml
      5cac408d
    • MARCHE Claude's avatar
      8e560e42
    • MARCHE Claude's avatar
      fix typo · 4725ff4c
      MARCHE Claude authored
      4725ff4c
    • MARCHE Claude's avatar
      rename split_intros_goal_wp into split_vc · 34aea94e
      MARCHE Claude authored
      34aea94e
    • MARCHE Claude's avatar
      7adf6371
    • MARCHE Claude's avatar
      0ac9d709
  3. 09 May, 2018 3 commits
  4. 07 May, 2018 4 commits