coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\|
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	We do up to `Term` which is the main bulk of the changes.
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \|	This will allow to merge back `Names` with `API.Names`
*	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\| \| \| \|	This is a first step towards some of the solutions proposed in #6008.
*	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \| \| \| \| \| \| \|	This is a second try at removing the hooks for the legacy xml export system which can't currently be tested. It is also not included in the API, so it should either be included in it or this PR be applied.
*	Further simplication: do not recreate entries for side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \|	This is actually useless, the code does not depend on the value of the entry for side-effects.
*	Remove a horrendous hack in Declare to retrieve exported side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \|	Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment.
*	More precise type of entries capturing their lack of side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \|	We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants.
*	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \|	We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
*	[general] Move files to directories matching linking order.	Emilio Jesus Gallego Arias	2017-07-19
	We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.