Merge requests · Why3 / why3 · GitLab

Mentions légales du service

coma: replace levels with a neutrality status + protected handler set

!1125 · created Sep 17, 2024 by Andrei Paskevich
- Merged
updated Sep 18, 2024
[WIP] use Dune 0 of 4 checklist items completed

!229 · created Sep 19, 2019 by François Bobot 1.9.0
component: build system
- 12
- 1
updated Sep 18, 2024
Resolve "Get rid of option `--json-values` in why3prove"

!1124 · created Sep 17, 2024 by Matteo Manighetti 1.7.3
ProofInUse/AdaCore
- Merged
- 7
updated Sep 18, 2024
fix session having extra edited files

!1126 · created Sep 18, 2024 by MARCHE Claude
- Merged
updated Sep 18, 2024
Resolve "fix usage of optional argument `me_name_trans` in functions on models"

!1122 · created Sep 17, 2024 by MARCHE Claude 1.8.0
ProofInUse/AdaCore component: counterexample
- Merged
updated Sep 19, 2024
Resolve "Add program equality on Boolean type"

!1121 · created Sep 17, 2024 by MARCHE Claude 1.8.0
component: theories
- Merged
updated Sep 19, 2024
Continue working on RAC log for incomplete case

!1103 · created Jul 11, 2024 by Matteo Manighetti
ProofInUse/AdaCore
- Merged
- 1
updated Sep 20, 2024
add "eval_match" to the Coma pipeline

!1128 · created Sep 23, 2024 by Andrei Paskevich
- Merged
updated Sep 23, 2024
new example for numeric strategy

!1129 · created Sep 26, 2024 by MARCHE Claude
ProofInUse/MERCE
- Merged
updated Sep 26, 2024
coma: eval_match expects all the implicit module imports

!1130 · created Sep 26, 2024 by Andrei Paskevich
- Merged
updated Sep 26, 2024
Resolve "IDE crashes when clicking on goal"

!1131 · created Sep 26, 2024 by MARCHE Claude 1.8.0
Creusot
- Merged
updated Sep 26, 2024
Resolve "why3 execute type inference problem"

!1127 · created Sep 19, 2024 by MARCHE Claude 1.8.0
component: execution
- Merged
updated Oct 01, 2024
Remove unneeded ghost qualifier

!1132 · created Oct 01, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Merged
updated Oct 01, 2024
Extraction tests fails due to non standard location of libgmp

!1097 · created Jul 03, 2024 by Gérald Point 1.8.0
- Closed
- 1
updated Oct 02, 2024
add a forgotten GMPFLAGS for targets that use GMP

!1108 · created Aug 09, 2024 by Gérald Point 1.8.0
component: examples
- Merged
updated Oct 02, 2024
Resolve "effect is now a keyword in OCaml 5.3"

!1135 · created Oct 02, 2024 by PATAULT Paul 1.8.0
- Closed
updated Oct 02, 2024
Add preliminary support for extraction of floating-point literals (fix #822).

!1099 · created Jul 04, 2024 by Guillaume Melquiond 1.8.0
ProofInUse/MERCE component: extraction
- Merged
- 1
updated Oct 02, 2024
Fix doc of extraction to C for records with mutable fields

!1138 · created Oct 02, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Merged
- 2
updated Oct 02, 2024
extraction to C: extract global variables

!1119 · created Sep 16, 2024 by MARCHE Claude 1.8.0
ProofInUse/MERCE
- Merged
- 8
updated Oct 02, 2024
js_of_ocaml version (5.6.0 minimum)

!1113 · created Sep 03, 2024 by PATAULT Paul 1.8.0
component: build system component: trywhy3
- Merged
- 3
updated Oct 03, 2024

Prev
1
…
52
53
54
55
56
57
58
59
60
61
Next