| Age | Commit message (Collapse) | Author |
|---|
|
We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
|
|
|
|
Add headers to a few files which were missing them.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.
Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.
Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.
cc: #7155
|
|
|
|
Not sure if worth using in other places.
|
|
|
|
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.
|
|
|
|
|
|
|
|
We reason up to order, and accept to match a final catch-all clauses
with any other clause.
This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
|
|
|
|
Up to this point the `lib` directory contained two different library
archives, `clib.cma` and `lib.cma`, which a rough splitting between
Coq-specific libraries and general-purpose ones.
We know split the directory in two, as to make the distinction clear:
- `clib`: contains libraries that are not Coq specific and implement
common data structures and programming patterns. These libraries
could be eventually replace with external dependencies and the rest
of the code base wouldn't notice much.
- `lib`: contains Coq-specific common libraries in widespread use
along the codebase, but that are not considered part of other
components. Examples are printing, error handling, or flags.
In some cases we have coupling due to utility files depending on Coq
specific flags, however this commit doesn't modify any files, but only
moves them around, further cleanup is welcome, as indeed a few files
in `lib` should likely be placed in `clib`.
Also note that `Deque` is not used ATM.
|
