Emilio Jesús Gallego Arias

@andres-erbsen thanks for your message, I agree with your vision. I think tho we are short of the technology / tooling needed to implement the challenges of this model in...

> > * there is no possibility to systematically explore the list of objects currently in scope (other than hoping the ad-hoc internal structures are somehow exposed) For this see...

I think this looks fine tho the issues in Coq seem largely orthogonal to the current argument parsing mechanism , see https://github.com/coq/coq/pull/8690 > This CEP is to address some of...

We have discussed cmdliner a few times, including https://github.com/coq/coq/issues/8818 , so I dunno. Unfortunately it won't work for Coq unless we want to drop compatibility with the current set of...

> This CEP is about sharing their declaration, parsing and printing. Well, this is where I am lost, AFAICS, having implemented already sharing of arguments between coqtop and coqc, I...

For the record this is the compat problem you would have with `cmdliner`: ``` {- [names] defines the names under which an optional argument can be referred to. Strings of...

See also https://github.com/coq/coq/pull/459 the diff may help to understand more some basic first steps.

> Goal forall n, n + 0 = n. > Proof. > elim. > - reflexivity. > - by move => n /= ->. > Qed. By the way the...

> Come on, there is no such thing as "the correct proof". I am not the best person to comment but indeed in math-comp there is a proof style, and...

Ok, so I've updated coq/coq#459 to a point where it is almost ready to handle the proper extends. We can continue the discussion about code there.