coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-12-15	Modify setoid_ring/Field_theory.v to compile with -mangle-names	Jasper Hugunin

2020-11-16	Improve some error messages.	Vincent Semeria
	This also includes aligning with refman when relevant and using capital letters and final period.
2020-10-11	Modify setoid_ring/Ring.v to compile with -mangle-names	Jasper Hugunin

2020-10-11	Modify setoid_ring/InitialRing.v to compile with -mangle-names	Jasper Hugunin

2020-10-08	Modify setoid_ring/Ring_polynom.v to compile with -mangle-names	Jasper Hugunin

2020-10-02	{new,setoid_}ring -> ring	Maxime Dénès
	I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-16	Modify setoid_ring/BinList.v to compile with -mangle-names	Jasper Hugunin

2020-09-16	Modify setoid_ring/Ring_theory.v to compile with -mangle-names	Jasper Hugunin

2020-04-17	Deprecate “omega”	Vincent Laporte

2020-04-03	Avoiding using a fixed introduction name in Ltac code of stdlib.	Hugo Herbelin

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias
	Currently, `.v` under the `Coq.` prefix are found in both `theories` and `plugins`. Usually these two directories are merged by special loadpath code that allows double-binding of the prefix. This adds some complexity to the build and loadpath system; and in particular, it prevents from handling the `Coq.*` prefix in the simple, `-R theories Coq` standard way. We thus move all `.v` files to theories, leaving `plugins` as an OCaml-only directory, and modify accordingly the loadpath / build infrastructure. Note that in general `plugins/foo/Foo.v` was not self-contained, in the sense that it depended on files in `theories` and files in `theories` depended on it; moreover, Coq saw all these files as belonging to the same namespace so it didn't really care where they lived. This could also imply a performance gain as we now effectively traverse less directories when locating a library. See also discussion in #10003