Guillaume Melquiond

> you may not want to automatically populate a name space by a mere application (e.g. `Module A := F B`) I think you do. As soon as a new...

For me, these two cases are the same primitive ("create a given name in a given namespace"), but it can indeed be called numerous times: once for creating the module...

> Not obvious to me, I think the opposite actually, namespace x exist iff there is a definition which prefix is x. This looks like a footgun: ```coq Module A....

> `raises a warning "empty namespace"` The fact that `Namespace A. End A. Open Namespace A.` can cause a warning is just awful, in my opinion. > Do we all...

> Regarding function extensionality, I don't remember if it derives back from the classical axiomatization It was not there in the original axiomatization. This dependency was only added when computable...

A point that troubles me is that the files `PArray`, `Sint63`, `Uint63`, `FloatAxioms` are moved outside of Coq. In my opinion, files that describe the computational behavior of Coq's kernel...

Here is my opinion on some of the choices: - Given `foo (A := bar) qux`, `qux` is used to fill the first non-implicit argument that occurs after `A`. All...

Right. The terminology "(non) dependent" is always confusing me. It would be clearer if it was "non-depended-upon argument", but I guess that would be too much of a mouthful in...

Are the following two sentences not contradictory? > We could in principle allow for more terms to qualify as symbols such as definitions (constants). > Rewrite rules are triggered when...

> but it would trigger once the left-hand side becomes a neutral term. It never becomes a neutral term, as it unfolds to a `fix` construct. > How do you...