5 Commits

Author	SHA1	Message	Date
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
BONNOT Paul	2e4dad7111	Improve the support for unbounded floats and forward error propagation strategy ... Unbounded floats theories for single resp double precision are now clones of a generic module parameterized by epsilon and eta Add support for exp and log in the strategy Add more examples of use in examples/numeric Documentation of the strategy in the manual Documentation of ufloat in the stdlib Documentation of session/strategy.mli in the API doc	2024-03-06 12:09:41 +01:00
BONNOT Paul	e4429e7dda	Resolve "Forward error propagation strategy : Sum, Exp, Log" ... new lemmas on real exp and log examples of use	2024-02-23 13:01:05 +01:00