Guillaume Melquiond

The shutdown has been pushed back to summer 2021.

> If you have an application where propositions such as foo need to be regularly solved, please let me know. Yes, we have a theorem where the issue appears all...

> One thing apparent from your example using `assert` and `backchain` is that it is possible to use `backchain` with a previous proved theorem and not just with an hypothesis...

> making intros also do left-asynchronous rules breaks all our existing example proofs That makes sense, and it explains why `intros` cannot be changed. But why not make `search` a...

> and picked a binary for which users are unlikely to have scripts. That is a incredibly optimistic statement. I never run Coqdoc by hand, it is always run through...

> Isn't Arg part of OCaml stdlib? Sure, but `Arg.Rest_all` is a very recent addition to the standard library, so it will not be available for most users.

What a waste. Clearing hypotheses might be the feature I miss the most from SSReflect when I am using Vanilla Coq, and now I learn it has actually existed for...

> It looks like it is actually useful, so should we document it as is? I don't think so. It would have made sense to do so in 2014. But...

This is a bug in GCC. As a consequence, the corresponding code in OCaml has been obfuscated to confuse the compiler, so as to disable the warning. That is, instead...

Yes, this is the standard behavior under Windows: "In text mode, CTRL+Z is interpreted as an EOF character on input." https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen