39 Commits

Author	SHA1	Message	Date
Claude Marche	01f80d6f50	relax hypothesis on a_max	2025-12-08 16:19:47 +01:00
Claude Marche	66a8b29530	improve proof of SLSE	2025-12-02 08:50:44 +01:00
Claude Marche	06c14de8b0	fixed slse proof	2025-11-24 17:21:15 +01:00
Claude Marche	7a655e6952	fixed lemma gg_bounds	2025-11-24 16:48:07 +01:00
Claude Marche	d17a7b64b7	redone sum_accuracy and g_accuracy	2025-11-24 11:33:09 +01:00
Claude Marche	13410bfc8f	cleaning	2025-11-24 11:22:11 +01:00
Claude Marche	9c60b5f0d6	add propagation in any format	2025-11-24 10:51:55 +01:00
MARCHE Claude	e802169b43	Improve numeric examples on exp and log	2025-10-08 12:18:30 +02:00
Claude Marche	d344b75294	fix proofs in subdir numeric ... make them replayed in bench	2025-09-30 13:34:10 +02:00
Claude Marche	816b76b5fe	Cleaning the proof and the doc comments for publications on the gallery	2025-03-14 15:25:29 +01: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	ae24b5d7fd	added LSE examples with fixed values for size	2024-11-15 17:29:45 +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
Claude Marche	3bb628674d	new example for numeric strategy	2024-09-24 15:14:35 +02:00
Claude Marche	052edfd29e	no need for FPa for these proofs	2024-09-02 11:13:06 +02:00
Paul Bonnot	4615f31920	Correct issue	2024-07-01 17:24:15 +02:00
Claude Marche	45f773f588	improve readibility, and various small improvements	2024-06-21 14:38:55 +02:00
Claude Marche	8dc497a29b	nicer post-condition for raytracer	2024-06-20 15:43:25 +02:00
Claude Marche	2cbd37f344	cleaning kinematics example	2024-06-20 12:01:06 +02:00
BONNOT Paul	f24be4fce6	SLSE example : simplify proof	2024-06-18 13:41:01 +02:00
Claude Marche	fb9cc77d53	clean the strategy code, use more reasonable approx of sin and cos	2024-06-11 14:06:18 +02:00