7 Commits

Author SHA1 Message Date
Jean-Christophe Filliatre
b8c5222cce new example: binary_multiplication with 63-bit integers 2018-10-04 16:47:09 +02:00
Andrei Paskevich
eae547d95f stdlib, examples: remove redundant "import" 2018-06-15 16:45:58 +02:00
Mário Pereira
54bfdf27e7 Binary_multiplication.mlw
div -> ( / )
2017-02-03 08:44:38 +01:00
Guillaume Melquiond
57d1a4be31 Merge branch 'master' into new_system
Conflicts:
	Version
	doc/manual.tex
	examples/add_list/why3session.xml
	examples/algo63/why3session.xml
	examples/algo64/why3session.xml
	examples/algo65/why3session.xml
	examples/all_distinct/why3session.xml
	examples/arm/why3session.xml
	examples/assigning_meanings_to_programs/why3session.xml
	examples/binary_multiplication.mlw
	examples/binary_multiplication/why3session.xml
	examples/binary_multiplication/why3shapes.gz
	examples/binary_search/why3session.xml
	examples/binary_sqrt/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/bubble_sort/why3session.xml
	examples/coincidence_count/why3session.xml
	examples/conjugate/why3session.xml
	examples/counting_sort/why3session.xml
	examples/cursor/why3session.xml
	examples/cursor/why3shapes.gz
	examples/defunctionalization/why3session.xml
	examples/dfa_example/why3session.xml
	examples/dfs/why3session.xml
	examples/fibonacci/why3session.xml
	examples/finite_tarski/why3session.xml
	examples/flag2/why3session.xml
	examples/gcd/why3session.xml
	examples/gcd_bezout/why3session.xml
	examples/gcd_bezout/why3shapes.gz
	examples/hackers-delight/why3session.xml
	examples/linked_list_rev/why3session.xml
	examples/mccarthy.mlw
	examples/mccarthy/why3session.xml
	examples/mccarthy/why3shapes.gz
	examples/patience/why3session.xml
	examples/power/why3session.xml
	examples/power/why3shapes.gz
	examples/queens_bv/why3session.xml
	examples/register_allocation/why3session.xml
	examples/schorr_waite/why3session.xml
	examples/schorr_waite/why3shapes.gz
	examples/sudoku/why3session.xml
	examples/verifythis_fm2012_treedel/why3session.xml
	modules/array.mlw
	share/emacs/why3.el
	share/latex/why3lang.sty
	src/core/pretty.ml
	src/core/task.mli
	src/driver/autodetection.ml
	src/printer/alt_ergo.ml
	src/tools/why3prove.ml
	src/transform/eval_match.ml
	src/transform/prepare_for_counterexmp.ml
	src/transform/split_goal.ml
	src/util/strings.mli
	src/why3session/why3session_html.ml
2016-06-16 08:23:43 +02:00
Jean-Christophe Filliatre
2ac91ce7e7 binary_multiplication: new-system-compliant code and a few comments 2016-06-02 17:00:43 +02:00
Claude Marche
a1e22351ee Update examples in progress 2016-03-09 15:22:02 +01:00
Jean-Christophe Filliatre
41cbd5c6cf new example: binary multiplication 2015-09-04 09:41:42 +02:00