9 Commits

Author	SHA1	Message	Date
Claude Marche	d344b75294	fix proofs in subdir numeric ... make them replayed in bench	2025-09-30 13:34:10 +02:00
Matteo Manighetti	7ae65be566	Upgrade sessions to use Alt-Ergo 2.6.0	2025-01-14 19:48:35 +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
BONNOT Paul	f24be4fce6	SLSE example : simplify proof	2024-06-18 13:41:01 +02:00
Paul Bonnot	fa655adbbf	Some LSE improvements	2024-06-10 17:48:06 +02:00
Paul Bonnot	2b743b654c	Correct sessions	2024-06-10 17:43:15 +02:00
BONNOT Paul	c602729144	New proofs of LSE and SLSE with modified strategy	2024-06-10 15:56:47 +02:00