189 Commits

Author	SHA1	Message	Date
Claude Marche	fc857b2fc2	proved udivexact generique	2025-11-25 11:26:25 +01:00
Claude Marche	b9feb6aece	proved mul generique	2025-11-25 10:49:15 +01:00
Claude Marche	d17a7b64b7	redone sum_accuracy and g_accuracy	2025-11-24 11:33:09 +01:00
Claude Marche	9c60b5f0d6	add propagation in any format	2025-11-24 10:51:55 +01:00
Jean-Christophe Filliatre	c928811d2d	map.MapPermut is a permutation	2025-05-07 23:43:38 +02:00
Claude Marche	e1d543c06f	SLSE full proof ... generalize hypothesis on size, depending on value of eps	2025-03-10 16:00:09 +01:00
Matteo Manighetti	7ae65be566	Upgrade sessions to use Alt-Ergo 2.6.0	2025-01-14 19:48:35 +01:00
Claude Marche	5f9169e032	fis sessions	2024-11-16 09:41:34 +01:00
Claude Marche	2e1d53f51b	fix sessions and CE oracles	2024-11-14 14:48:30 +01:00
Claude Marche	c000797178	Additional operators for fmaps	2024-11-08 10:15:33 +01:00
MARCHE Claude	4d04b4f698	add metas for unused-dependencies on sequences ... also fix split_full that was losing metas for unused dependency	2024-10-29 16:12:46 +01:00
MARCHE Claude	9161acda8e	Add metas for unused dependencies in generated axioms	2024-10-25 18:34:29 +02:00
Claude Marche	27fb33580e	Support for Coq 8.19.2	2024-10-03 11:19:54 +02:00
MARCHE Claude	6813754dce	clarify ghost and non-ghost for reals and ufloats	2024-10-01 15:38:42 +02:00
MARCHE Claude	6e3d21b5f0	check that real.FromInt.from_int is correctly sent to Alt-Ergo ... updated sessions	2024-09-17 10:44:53 +02:00
PATAULT Paul	9371ad18ab	Merge branch 'coma-only' into 'master' ... New front-end language: Coma See merge request why3/why3!1098	2024-09-04 10:19:12 +02:00
MARCHE Claude	59cb8a7de0	List length via peano	2024-09-03 11:09:30 +02:00
Paul Patault	bf775596c8	coma: generalize let%attr in let%span ... + creusot patches + CI patches	2024-08-08 11:09:30 +02:00
Jacques-Henri Jourdan	3f74341ea3	Remove redondancy of bv_size definition in mach.bv. ... This was essentially defined twice : once in bv and once in mach.bv.	2024-07-15 13:48:41 +02:00
Claude Marche	45f773f588	improve readibility, and various small improvements	2024-06-21 14:38:55 +02:00
MARCHE Claude	016ab0186e	Merge branch 'coq_deprecated_omega' into 'master' ... update Coq proofs using lia instead of omega See merge request why3/why3!1087	2024-06-18 15:55:29 +02:00
BONNOT Paul	f24be4fce6	SLSE example : simplify proof	2024-06-18 13:41:01 +02:00
Claude Marche	341f530df1	update Coq proofs using lia instead of omega	2024-06-18 13:38:53 +02:00
Paul Bonnot	7c3e02999d	Remove higher order	2024-06-10 16:44:04 +02:00
Claude Marche	bcf91c0e6e	updated coq proofs	2024-05-31 14:17:56 +02:00