| Age | Commit message (Collapse) | Author |
|---|
|
Add headers to a few files which were missing them.
|
|
Ack-by: JasonGross
Ack-by: MSoegtropIMC
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Most of these files were introduced after #6543 but used older headers
copied from somewhere else.
|
|
Most functions are taken either from the Coq standard library or the
OCaml standard library. One (`enumerate`) is taken from Python. Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception). Since `exists` is a keyword, we use the
Coq name `existsb` instead. We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.
Note that `seq` matches neither Coq nor OCaml; it takes a `step`
argument for how much to increment by on each step.
Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?
|
|
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
|
