Description of the problem

The following code does not raise an error, and the behavior is undocumented.

Section Test.
Variables (b : bool) (n : nat) (All : unit).
Collection n := b.

Lemma foo : True.
Proof using n.
trivial.
Qed.

Lemma bar : True.
Proof using All.
trivial.
Qed.
End Test.

Check foo : bool -> True.
Check bar : bool -> nat -> unit -> True.

This is very low prio, but it usually happens that when touching Prims or some other file high in the dependency graph, we get spurious diffs in many other files. Since we check-in the snapshot, and we need to have it up-to-date, we get very verbose commits when nothing relevant changed. Plus, when something did change, it's hard to spot.

Example: I removed a few lines in prims and get things

This issue is not urgent. I open it to keep it in mind.

Many tools use http://www.sphinx-doc.org/ now for their doc, including Coq. See https://coq.inria.fr/distrib/current/refman/ . It seems to be automatically generated from html and http://docutils.sourceforge.net/rst.html files in https://github.com/coq/doc.

Perhaps we should do the same to get a better rendering of the doc.

Eval cbn in 1 + 1.
Definition x :=
  Eval cbn in 1 + 1.
Definition y := 2.

The second Eval is not highlighted, and the second Definition is indented to match the second Eval.

search [issue 7] in code for background, or see this commit 1855e9218c7388ce1b4bf1f19d6679fcaea2324c

this issue only touch the parser and elaborator, don't touch the core