5 Commits

Author	SHA1	Message	Date
Andrei Paskevich	eae547d95f	stdlib, examples: remove redundant "import"	2018-06-15 16:45:58 +02:00
Andrei Paskevich	d23e9cd8a2	use "return" in several examples	2017-06-06 02:13:01 +02:00
Jean-Christophe Filliatre	f868ab16f7	updated proof sessions	2017-05-16 15:48:09 +02:00
Jean-Christophe Filliatre	397e8c4d7d	gallery: more proofs of termination	2014-01-22 18:13:40 +01:00
Andrei Paskevich	4b1bc2b0c0	reorganize examples/ ... - all programs with sessions are in examples/ - all programs without sessions are in examples/in_progress/ (if you have private sessions for those, just move them there) - all pure logical problems are in logic/ (to simplify bench scripts and gallery building; they are few anyway) - all OCaml programs are in examples/use_api/ - all strange stuff is in examples/misc/ (most of it should probably go) - Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/ (why do we need two sets of solutions for quite simple problems?) - hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/ Bench scripts and documentation are updated. Also, bench/bench is simplified a little bit.	2013-01-30 01:23:44 +01:00