coq - The formal proof system

Age	Commit message (Collapse)	Author
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-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-06-06	STM: support for nested boxes of nodes to model error boundaries	Enrico Tassi
	Dag extended to support arbitrary clusters, renamed to Property. Vcs generalized to not impose the data hold by a Property. Stm(VCS) names a property "a box" and imposes a topological invariant (no overlap). It defines 2 kind of boxes: ProofTasks (the old cluster notion) and ErrorBound (meant to confine errors to sub-proofs). In the meanwhile more equations added to Make(..) functors in order to have just one Stateid.Set module around.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-04-25	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot
	files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.