Benjamin Jorge
a07a1b6a88
Improve Pmodule API, update documentation
2025-11-20 14:14:24 +01:00
Benjamin Jorge
667ab3ae79
Sandwich implementation
2025-11-20 14:14:24 +01:00
Claude Marche
e991d73789
update headers
2025-06-04 10:51:30 +02:00
Guillaume Melquiond
8a86d9ac62
Update copyright years.
2024-12-07 09:01:55 +01:00
Guillaume Melquiond
edc8798d88
Replace Opt functions that are provided by the standard library.
2023-11-23 14:26:27 +01:00
Guillaume Melquiond
79738ae6a4
Update headers.
2023-03-07 09:58:45 +01:00
MARCHE Claude
a23f364805
Resolve "wish: use a multi-line format for source locations"
2022-06-22 18:17:43 +00:00
Guillaume Melquiond
53926bbbf5
Update headers.
2022-04-26 16:33:42 +02:00
Guillaume Melquiond
55fc17a4ea
Change interface-only .ml files into .mli files.
2021-09-28 18:05:52 +02:00
Guillaume Melquiond
f75492a0db
Remove dead code.
2021-09-28 17:32:00 +02:00
Guillaume Melquiond
ebfa10f2b9
Silence warning 70 "missing-mli".
...
OCaml warns when there is a .ml file but no .mli file. This commit adds
almost all the missing .mli files. The remaining ones are the *_ast.ml
files, as the .mli files would be verbatim copies.
2021-09-28 17:32:00 +02:00
Jean-Christophe Filliatre
01d152077f
micro-C: fixed detection of unbound variables in assignments
2021-09-15 10:59:30 +02:00
Guillaume Melquiond
534dcdd5f5
Do not call fprintf when the string does not contain any format modifier.
2021-09-10 14:11:20 +02:00
Guillaume Melquiond
1fc6be8459
Update headers.
2021-03-13 07:55:14 +01:00
Jean-Christophe Filliatre
6afec7fed1
removed trailing whitespaces
2020-06-24 23:04:08 +02:00
Jean-Christophe Filliatre
cff973030c
micro-C/Python: fixed translation of <> and not
2020-06-24 22:19:17 +02:00
Guillaume Melquiond
0070b9408d
Update headers.
2020-03-17 09:52:33 +01:00
Jean-Christophe Filliatre
0621f1be18
micro-C: quantifiers on both integers and arrays
2020-01-25 08:27:13 +01:00
Jean-Christophe Filliatre
ed43fdc41e
micro-C: better error message on a missing return
2020-01-24 09:48:43 +01:00
Jean-Christophe Filliatre
ec137ced0d
micro-C: fixed minor issues
...
C types are now taken into account, instead of having Why3 infer types
new declarations lemma/goal/axiom : term
2020-01-24 09:24:03 +01:00
Sylvain Dailler
4bc6f56060
microc: add simple cases for external printing/parsing
2019-12-06 10:31:55 +01:00
Cláudio Belo Lourenço
83b02e04ac
Merge branch 'master' into 28-string-literals
2019-10-21 15:05:46 +02:00
Cláudio Belo Lourenço
372ec5a396
All constant literals under the same data type: integer, reals, and strings
2019-09-20 10:42:31 +02:00
Cláudio Belo Lourenço
c7a09d626b
Wrapping all constant literals under the same construct.
...
Strings not supported in this commit.
2019-09-19 20:14:54 +02:00
Raphael Rieu-Helft
f2a95dad7e
Make alias work with named returns
2019-09-19 15:58:19 +02:00
