Cyril Cohen

Replace check for existing binaries in cache

2

This is dirty! https://github.com/coq-community/coq-nix-toolbox/blob/5e713b1b2be756cd5d9b6df6615390e772ff1dfb/.nix/shellHook.sh#L204-L205

https://github.com/coq-community/coq-nix-toolbox/blob/ab43447ff01c2ccf712f14aca5b99d14e5735440/.nix/shellHook.sh#L154 One way to do it is to pass only the selection, via task cf #7

https://github.com/coq-community/coq-nix-toolbox/blob/b1e5c52bdc1d79b7cd220476ebd9bc552a2331c7/project-default.nix#L1

Equivalence with usual stability

2

"Usual" stability is equivalent to "lexicographic" stability

Remove the phantom in tuple

1

##### Motivation for this change Simplify the code base using reverse coercions ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation...

Missing lemma from `@ball subspace` to the definition of `subspace_ball`

E.g. `Search _ in bigop` lists the contents of the submodule `bigop` defined in order to make bigop definition opaque, while the user intent is to list the contents of...