ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
18,511 Commits 65 Branches 1 Tag
master
Commit Graph

546 Commits

Author SHA1 Message Date
Johannes Kanig
25b13e2cab merge commit 2025-12-15 10:45:08 +09:00
Benjamin Terra-Jorge
b7058e58c1 Merge branch '910-distinct-theories-with-the-same-ident' into 'master' 
Resolve "Distinct theories with the same ident"

Closes #910

See merge request why3/why3!1214
 2025-12-10 09:13:49 +00:00
Guillaume Melquiond
4b24da8c83 Remove some admits in Coq realizations. 2025-11-27 09:42:21 +01:00
Benjamin Jorge
cb0a4a1e60 Fix coq realizations 2025-11-20 14:11:25 +01:00
Johannes Kanig
a2807b3ddb Merge 1.8.2 into AdaCore master 2025-10-14 10:32:03 +09:00
MARCHE Claude
609cd64dae Fix build with Rocq Stdlib 9.0 
Contributed by Josselin Poiret
 2025-09-17 17:03:24 +02:00
Claude Marche
506efc97c6 update ae version for CE checking 2025-09-15 15:03:51 +02:00
Claude Marche
9edb02fc65 Fix build with Rocq Stdlib 9.0 
Contributed by Josselin Poiret
 2025-09-15 14:01:08 +02:00
MARCHE Claude
ff86d53bf2 Produce special float values in counterexamples 2025-06-11 13:09:37 +02:00
Claude Marche
50f084bf55 Merge branch 'bugfix/v1.8' 2025-06-04 11:10:16 +02:00
Claude Marche
e991d73789 update headers 2025-06-04 10:51:30 +02:00
Jean-Christophe Filliâtre
53b3249062 list.Distinct using a recursive definition 2025-05-14 17:32:28 +02:00
Johannes Kanig
7fc06eaa52 Revert "get rid of deprecated module Arith.Div2" 
This reverts commit bf71827e9c.
 2025-03-31 09:35:26 +09:00
MARCHE Claude
997bdc53c1 add simple examples of iterators on sets with extraction to OCaml 
The stdlib is augmented with iterator mechanisms

The OCaml extraction driver is augmented accordingly, using OCaml Seq
 2025-03-26 17:20:01 +01:00
Matteo Manighetti
c04b008016 Merge remote-tracking branch 'why3-inria/master' into why3-devel 2024-12-13 17:34:11 +01:00
Guillaume Melquiond
8a86d9ac62 Update copyright years. 2024-12-07 09:01:55 +01:00
Claude Marche
cabea44347 fix realizations 2024-11-13 19:10:42 +01:00
Guillaume Melquiond
35601b77e7 Switch to zarith (fix #298). 2024-11-08 22:05:42 +01:00
Guillaume Melquiond
a7d0370df3 Add missing Coq definition for BuiltIn.string. 2024-11-08 13:48:11 +01:00
MARCHE Claude
5ced5ae2b7 Adding a function from_real in the theory of IEEE floats 2024-11-03 21:13:10 +01:00
MARCHE Claude
6ce01d8b7e Resolve "provide axioms for sdiv and smod in theory bitvector theory" 2024-11-02 08:36:31 +01:00
Matteo Manighetti
1c65544ddb Merge commit '1dc1b78e8c8e39e7b57e7299be0879ed027d19bd' into why3-before-cex-from-rac 2024-10-23 16:51:58 +02:00
Claude Marche
bf71827e9c get rid of deprecated module Arith.Div2 2024-06-20 12:02:53 +02:00
Guillaume Melquiond
938d1dd37d Partly adapt to Coq 8.19. 
These changes are still compatible with Coq 8.13.
 2024-04-22 17:19:50 +02:00
Claude Marche
4bd2a48d56 add isabelle proofs for new axioms and lemmas in real.ExpLog 2024-04-17 14:22:39 +02:00