coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[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`
*	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\| \| \| \| \|	When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Pretyping cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
\|
*	[stm] Break stm/toplevel dependency loop.	Emilio Jesus Gallego Arias	2017-02-15
	Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore.