Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
6dc3d5a2
Commit
6dc3d5a2
authored
Oct 05, 2018
by
Guillaume Melquiond
Browse files
Update changes.
parent
075df85c
Changes
1
Hide whitespace changes
Inline
Side-by-side
CHANGES.md
View file @
6dc3d5a2
:x: marks a potential source of incompatibility
Version 1.1.0, ...
------------------
Core
*
variants can now be inferred on some lemma functions
*
coercions are now supported for
`if`
and
`match`
branches
Language
*
program functions can now be marked
`partial`
to prevent them from
being used in ghost context; the annotation does not have to be
explicitly put on their callers
*
`use`
now accepts several module names separated by commas
*
symbolic operators can be used in identifiers like
`(+)_ident`
or
`([])'ident`
Standard library
*
floating-point functions from
`ieee_float`
can now be used in programs
Transformations
*
`split_vc`
behaves slightly differently :x:
Provers
*
support for Alt-Ergo 2.1.0 (released Mar 14, 2018)
*
support for Alt-Ergo 2.2.0 (released Apr 26, 2018)
...
...
@@ -51,6 +72,7 @@ Language
Standard library
*
machine integers in
`mach.int.*`
are now range types :x:
*
added a minimal memory model for the C language in
`mach.c`
*
new modules
`witness.Witness`
and
`witness.Nat`
Extraction
*
improved extraction to OCaml
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment