coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-10	[ocamlformat] Enable for funind.	Emilio Jesus Gallego Arias
	As part of the proof refactoring work I am doing some modifications to `funind` and indentation of that code is driving me a bit crazy; I'd much prefer to delegate it to an automatic tool.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-31	[funind] Port invfun to the new tactic engine.	Emilio Jesus Gallego Arias

2019-07-31	[funind] Derive_correctness is only used in funind, thus more there.	Emilio Jesus Gallego Arias

2019-07-15	[funind] Remove unneeded callback.	Emilio Jesus Gallego Arias

2019-06-24	Duplicate the type of constant entries in Proof_global.	Pierre-Marie Pédrot
	This allows to desynchronize the kernel-facing API from the proof-facing one.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
	- move_location to proofs/logic. - intro_pattern_naming to Namegen.
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
	In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-01-24	Remove dead code from funind.	Maxime Dénès