| Age | Commit message (Collapse) | Author |
|---|
|
Many still remain.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
|
"rename" flag
|
|
|
|
|
|
|
|
|
|
|
|
|
|
kernel closures.
|
|
pattern-matching names
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
|
tactic unification.
|
|
|
|
coinductive types.
|
|
|
|
|
|
|
|
of List
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Note that one of them is in the name of the main theorem, so we use a
compatibility notation.
|
|
patterns with different variables
|
|
|
|
|
|
|
|
|
|
Still some discrepancies though. E.g.:
- some functions taking an equality as arguments have suffix `_f` but
not all;
- the functions possibly raising an error have still different kinds
of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange,
and when in the first two cases, with no unique rules in the style
of the associated string - we thus avoid to document the exact
string used).
There are a few semantics changes:
- skipn_at_least now raises a `Failure` if its argument is negative;
- map3 raises an Invalid_argument "List.map3" rather than
Invalid_argument "map3" and similarly for map4
- internally, map3 and map4 are now tail-recursive (by uniformity);
- internally, split3 and combine3 are now tail-recursive (by uniformity);
- filter is now "smart" by default and smartfilter is deprecated;
- smartmap is now tail-recursive by default.
|
|
|
