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] Remove export of `generate_functional_principle` and `make_scheme`	Emilio Jesus Gallego Arias
	This removes the export of two internal functions, moving to their only use place. In particular, `make_scheme` was exposing the low-level `proof_entry` object, which should not do. This will allow to refactor all these constant-building functions towards a more uniform use of the API. In particular, all the functions manipulating proof entries directly are in `Gen_principle`.
2019-07-31	[funind] Move principle generation to its own file.	Emilio Jesus Gallego Arias