Commit 9bd7c976 authored by François Bobot's avatar François Bobot

Update doc and CHANGES during GT

parent b48534a4
......@@ -25,6 +25,7 @@ Language
Flanagan-Saxe-like VC generation
* support for type coercions in logic using `meta coercion`
* deprecated `theory`; use `module` instead
* term on the left of sequence `;` must be of type `unit` :x:
Standard library
* machine integers in `*` are now range types :x:
......@@ -290,11 +290,20 @@ egalite sur les type algebriques ? engendrees automatiquement ?
\subsection{Syntax Changes}
Logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type \texttt{int} in the standard library). The CHANGES
file contains other potential incompatibility.
\textbf{version 0.87} & \textbf{version 0.90} \\
\texttt{function f ...} & \texttt{let function f ...} if called in
programs \\
\texttt{'L:} & \texttt{label L in} \\
\texttt{at x 'L} & \texttt{x at L} \\
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment