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
Claude Marche
4d68a5a802
disabled Alt-Ergo FPA for versions < 2.5.4 (bug known)
2024-05-23 11:17:31 +02:00
MARCHE Claude
85916f62c6
never encode enums and records for Alt-Ergo
2024-05-22 12:18:37 +02:00
Paul Bonnot
103af257d0
Removed inline_trivial
2024-04-22 17:41:45 +02:00
Claude Marche
2a1637b43d
remove useless hint
2024-04-16 12:58:50 +02:00
BONNOT Paul
79666d1218
Resolve "forward_propagation strategy : sin and cos support"
2024-03-28 15:49:24 +01: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
