8 Commits

Author	SHA1	Message	Date
Andrei Paskevich	3a9ea01ed9	Matrix: add the pure "update" function for applicative updates	2018-07-02 17:15:42 +02:00
Andrei Paskevich	5130cf4361	update CHANGES + some cosmetics	2018-06-24 14:39:47 +02:00
Andrei Paskevich	eae547d95f	stdlib, examples: remove redundant "import"	2018-06-15 16:45:58 +02:00
Andrei Paskevich	fb77f39422	Vc: no more "liberal_for" ... Instead, we put a "stop_split" over the subsequent postcondition under the (begin > end + 1) assumption. When this assumption is unrealizable (strict for), this allows us to discharge the whole branch as a single goal.	2017-05-22 16:28:07 +02:00
Jean-Christophe Filliatre	63b8f6d0f4	updated proof sesssions	2017-05-16 14:22:45 +02:00
Guillaume Melquiond	7d060891b9	Merge branch 'master' into new_system	2017-05-15 14:26:58 +02:00
Jean-Christophe Filliatre	790d613404	binary sort: simplified code (and proof) using self_blit	2017-04-20 11:05:33 +02:00
Jean-Christophe Filliatre	98cf448bdd	new examples: tree_of_array and binary_sort	2017-04-20 10:34:47 +02:00