16 Commits

Author	SHA1	Message	Date
Matteo Manighetti	c04b008016	Merge remote-tracking branch 'why3-inria/master' into why3-devel	2024-12-13 17:34:11 +01:00
Guillaume Melquiond	35601b77e7	Switch to zarith (fix #298).	2024-11-08 22:05:42 +01:00
Matteo Manighetti	1c65544ddb	Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac	2024-10-23 16:51:58 +02:00
Paul Patault	b7d4770c7d	coma: simplify examples	2024-10-17 20:00:12 +02:00
Paul Patault	bf775596c8	coma: generalize let%attr in let%span ... + creusot patches + CI patches	2024-08-08 11:09:30 +02:00
Paul Patault	23f1a47aae	coma: proto let%attr let%file	2024-08-08 09:06:08 +02:00
Andrei Paskevich	4ab78a9f61	coma: eliminate trivial equalities more aggressively	2024-08-08 09:06:08 +02:00
Paul Patault	25de89f4cc	coma: tests with polymorphism	2024-08-08 09:06:08 +02:00
Andrei Paskevich	6be7f4230d	coma: minor	2024-08-08 09:06:08 +02:00
Paul Patault	66d39526c1	coma: syntax update && polymorphism (wip)	2024-08-08 09:06:07 +02:00
Jean-Christophe Filliatre	54712b24ac	new coma example using binary search trees	2024-08-08 09:06:07 +02:00
Andrei Paskevich	89a52ee2af	coma_vc: rework factorization	2024-08-08 09:06:07 +02:00
Andrei Paskevich	47ef2080db	coma_vc: alternative implementation	2024-08-08 09:06:07 +02:00
Paul Patault	6e64c3e3c7	coma: extension parser + pretty printer	2024-08-08 09:06:07 +02:00
Matteo Manighetti	343864754e	Use Option from standard library	2024-01-22 16:43:44 +01:00
MARCHE Claude	72a423af11	move examples in progress outside the examples directory	2023-03-08 12:26:34 +00:00