This works fine in Nix because those package names are the names of derivations that themselves pin a given version of said packages. In practice, the default set is expected to be somewhat internally consistent, so…
Thanks, this is very interesting and I'd love to switch to 8.5. I might wait a little for my benchmarks to be 8.5 ready though!
Indeed trying tactics in general can be unsatisfactory if you 1) don't let users enrich the set of tactics tried 2) don't let users prevent some things from being tried. For your other issue, I am thinking about ways to…
I've always wondered why people building vim support for Coq did not name it Coq-au-vim...
This works fine in Nix because those package names are the names of derivations that themselves pin a given version of said packages. In practice, the default set is expected to be somewhat internally consistent, so…
Thanks, this is very interesting and I'd love to switch to 8.5. I might wait a little for my benchmarks to be 8.5 ready though!
Indeed trying tactics in general can be unsatisfactory if you 1) don't let users enrich the set of tactics tried 2) don't let users prevent some things from being tried. For your other issue, I am thinking about ways to…
I've always wondered why people building vim support for Coq did not name it Coq-au-vim...