coqbot

Comment author: @robbertkrebbers What is the current status of cbn? Does it support all features of simpl (like those set using Arguments)? Will simpl be deprecated/removed in 8.5 in favor...

Comment author: @pirbo > What is the current status of cbn? Sadly, a bit "in the middle of the way". > Does it support all features of simpl > (like...

Comment author: @robbertkrebbers What kind of incompatibilities can one expect?

Comment author: @gares I think we should recommend it, but not remove simpl since scripts may depend on its weird behavior. Just one example, if you have f(x) and x...

Comment author: @pirbo Sorry for the delay. I've tried to explain the main differences in this draft : https://hal.archives-ouvertes.fr/hal-00816918 I should try to resubmit something more complete this year ...

Comment author: @robbertkrebbers In Coq 8.5 cbn does not fold the mutual fixpoint in the second example. So: ```coq Section help. Context (i : nat). Fixpoint foo (n : nat)...

Comment author: @Lionel-Rieg In addition to the current explanations, I think the following information should be added to the page describing Coq installation via opam: - Make sure that the...

Hi, If I try do build the following module, I get an error message "Signature components for label Ia do not match". But if I replace the inductive definition of...

Now the error message is more explicit : User error: The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename...

Comment author: @pirbo It will be for the next rewriting of the kernel from scratch...