coq - The formal proof system

Age	Commit message (Collapse)	Author
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-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-09-04	Make `Print Rings` and `Print Fields` reliable	Maxime Dénès
	Previously, they were using a map that was different from the one used by the real lookup, leading to confusing information (number of instances could be wrong, etc).
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-06-18	Remove reference name type.	Maxime Dénès
	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
2018-03-10	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias
	Unfortunately, mli-only files cannot be included in packs, so we have the weird situation that the scope for `Tacexpr` is wrong. So we cannot address the module as `Ltac_plugin.Tacexpr` but it lives in the global namespace instead. This creates problem when using other modular build/packing strategies [such as #6857] This could be indeed considered a bug in the OCaml compiler. In order to remedy this situation we face two choices: - leave the module out of the pack (!) - create an implementation for the module I chose the second solution as it seems to me like the most sensible choice. cc: #6512.