coq - The formal proof system

Age	Commit message (Collapse)	Author
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.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-11-06	Checker now disables VM and native	Maxime Dénès
	At the same time, we made the safe_env threading explicit.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-11-29	Allow to pass physical files to coqchk.	Pierre-Marie Pédrot

2017-11-28	Adding an interface file for checker/check.ml.	Pierre-Marie Pédrot