Pierre Rousselin
Pierre Rousselin
As a use case, assume `alice` has a local copy of the `coq` repository. She does something like this: ```shell-session $ echo $COQBIN /home/alice/coq/_build/install/default/bin $ autoconf ``` and then `autoconf`...
Thank you. I think that `COQBIN`, if set and non empty usually has priority over the `PATH`. Then if the user prefers to build it against a released version in...
> see also #11876 The issue seems to still be there... So what's the intended behaviour? Do we want the last command here to compile? ```coq Module Type type1. Parameter...
@coqbot run full ci
I have made some progress on it. Waiting for feedback before triggering the full ci.
@coqbot run full ci
@coqbot run full ci
@coq/vernac-maintainers Do you think this PR is ready, or are there other things to take care of?
Mostly to @andres-erbsen: - I've renamed `Even_Odd_induction` into `binary_induction` - I've renamed `le_shiftl` and `shiftr_le` into, respectively `shiftl_lower_bound` and `shiftr_upper_bound` - For `div2 a
Thank you! If you don't mind, I would also like to: - [x] change `binary_induction` (and redefine it without the spurious `Proper` clause in implementations) so that it can be...