• Ralf Jung's avatar
    Remove the `default` notation for options · e585be6d
    Ralf Jung authored
    The notation was parsing-only and all it did was reorder the arguments for
    from_option.  This creates just a needless divergence between what is written
    and what is printed.  Also, removing it frees the name for maybe introducing a
    function or notation `default` with a type like `T -> option T -> T`.
    e585be6d
Name
Last commit
Last update
ci @ 99c935d2 Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
CONTRIBUTING.md Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
awk.Makefile Loading commit data...
descr Loading commit data...
opam Loading commit data...