7 Commits

Author	SHA1	Message	Date
Guillaume Melquiond	ea123b5e95	Improve documentation of standard library.	2021-09-21 18:00:14 +02:00
Jean-Christophe Filliatre	0a5c1e5c0b	queue.Queue: changes and documentation	2019-06-06 17:45:36 +02:00
Jean-Christophe Filliatre	dce06eef11	library queue.Queue: fixed spec of pop	2019-06-05 17:34:13 +02:00
zapashcanon	691be6d276	queue spec update with seq	2019-06-05 14:43:53 +02:00
Jean-Christophe Filliatre	43b40a4866	library: {Stack,Queue}.length now return a Peano.t ... this way, the extraction maps them to OCaml's {Stack,Queue}.length without using ZArith anymore	2018-10-26 15:47:03 +02:00
Andrei Paskevich	eae547d95f	stdlib, examples: remove redundant "import"	2018-06-15 16:45:58 +02:00
Guillaume Melquiond	efb51e7d43	Merge theories and modules into stdlib (fix issue #62).	2017-12-15 15:34:35 +01:00