Gabriel Scherer
Gabriel Scherer
Hi all, Do you have any news of potential progress on this issue? Today, if I go to a random page of the manual, for example , I still don't...
This is still an issue for me, every time I need to access the reference manual to provide an URL for other people.
(I mentioned the manual again today and was reminded of this issue.)
Thanks! This sounds like it fixes the problem for me: if I browse the manual through the web, I will end up on a URL that I can easily tweak...
In this issue a lot of potential UI choices were discussed to show this flexibility to users (let them jump to another version, or ask for the latest version, get...
This issue was reported again [on Discuss today](https://discuss.ocaml.org/t/what-are-the-biggest-reasons-newcomers-give-up-on-ocaml/10958/186), it looks like several libraries are affected with authors reporting that the documentation of their code on ocaml.org is missing content. (cc...
In the case of `Axiom`, there is a clear notion of what it means to realize an axiom: provide a term of the axiomatized type . In some cases a...
Sometimes we would sketch a development by axiomatizing a part of the theory, hoping to prove later than the axioms can in fact be realized. (In practice I think people...
For the record, I am not so convinced by @silene's point in general. It looks very cumbersome to have to first define one axiom per symbol and equation, and then...
So instead of ```coq Rewrite Block := plus : nat -> nat -> nat ; with rules plus 0 ?n := n ; plus ?n 0 := n ; plus...