Benjamin Terra-Jorge
8bb9da3b6b
Merge branch '894-extraction-broken-when-cloning-a-module-with-interface' into 'master'
...
Resolve "Extraction broken when cloning a module with interface"
Closes #894
See merge request why3/why3!1190
2025-12-10 09:20:51 +00:00
Li-yao Xia
d43e0a0332
'informations' -> 'information'
2025-11-28 11:05:21 +01:00
Benjamin Jorge
a07a1b6a88
Improve Pmodule API, update documentation
2025-11-20 14:14:24 +01:00
Claude Marche
e5f6a089fe
fix doc of for loops
2025-11-19 13:18:39 +01:00
MARCHE Claude
81affec0ed
Merge branch 'lident_doc' into 'master'
...
doc: exclude '_' from lident_nq
See merge request why3/why3!1222
2025-10-17 17:01:47 +02:00
Claude Marche
d949b4639b
make output of Kim accent simpler
2025-10-17 10:52:15 +02:00
MARCHE Claude
e053e2ef6b
update after release 1.8.2
2025-09-15 13:38:49 +02:00
Claude Marche
50f084bf55
Merge branch 'bugfix/v1.8'
2025-06-04 11:10:16 +02:00
Claude Marche
b9fe989f75
Version 1.8.1
2025-06-04 10:59:28 +02:00
Claude Marche
4a95bf2863
prepare release
2025-06-04 10:49:46 +02:00
Li-yao Xia
9cd080a32f
doc: exclude '_' from lident_nq
2025-05-13 10:48:09 +02:00
Guillaume Melquiond
6db1a4816f
Merge branch 'bugfix/v1.8'
2025-05-02 15:51:23 +02:00
Li-yao Xia
0687abff5e
doc: Fix production rules for suffix, lident_nq, uident_nq, qident to agree with lexer.mll
2025-04-09 15:46:38 +02:00
Matteo Manighetti
7b3ec0ad7d
Check_ce: simplify API interface
...
All functions in Check_ce now assume that counterexample checking
has been requested. Two entry functions are provided, to request
both small and giant step RAC (useful for checking WhyML programs)
or to only request giant step RAC (useful when the small-step will
be performed on another language).
The RAC log is returned, and should be interpreted to produce a
counterexample. As a temporary helper, an incomplete model is also
returned, that contains all the values extracted from the log.
2025-02-10 18:20:22 +01:00
Guillaume Melquiond
3f66c6e298
Use more links to the standard library in the documentation.
2024-12-16 15:49:10 +01:00
Guillaume Melquiond
59fde1a829
Fix some documentation typos.
2024-12-16 15:49:10 +01:00
Guillaume Melquiond
187fd52100
Version 1.8.0
2024-12-11 14:21:37 +01:00
Jean-Christophe Filliâtre
93d4646a98
improved documentation
2024-11-27 15:38:02 +01:00
Jean-Christophe Filliâtre
da82f89b3f
Merge branch 'whyml2java' into 'master'
...
Whyml2java
See merge request why3/why3!1064
2024-10-31 21:14:12 +01:00
Jean-Christophe Filliatre
f09af29a43
reviewing whyml2java
...
typos in doc, trailing white space, gitignore
2024-10-31 17:51:38 +01:00
Claude Marche
227c5c7b8c
also output type definitions and logic definitions
...
Although, only algebraic type definitions are printed
2024-10-18 12:02:19 +02:00
MARCHE Claude
a74598f928
do not take resource limits from more than one source
2024-10-08 21:00:00 +02:00
MARCHE Claude
05f9f6c3a1
Fix doc of extraction to C for records with mutable fields
2024-10-02 19:06:12 +02:00
Gerald Point
3aaff7c032
documentation of the Java extraction
2024-10-02 11:28:58 +02:00
Hugo Gimbert
a0fa93f049
added first draft of whyml2java spec
2024-10-02 11:28:58 +02:00
