coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-27	Release notes for 8.12.	Théo Zimmermann

2020-05-22	[coqchk] Fix #5030	Pierre Roux
	When encountering ```Coq Module M : T. ... Lemma c :... ... Qed. ... End M. ``` every field `c` without body in `T` but with a body in `M` is registered as opacified in a table along with all constants `opacified(c)` without body in the environment at this point (i.e., all axioms potentially used by c). Then, when printing axioms, if `c` appears in the final environment it is replaced by `opacified(c)` in the resulting list of axioms.