coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\| \| \| \|	We address the easy ones, but they should probably be all removed.
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
\| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[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.
*	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
\|
*	Getting rid of AUContext abstraction breakers in Search.	Pierre-Marie Pédrot	2017-07-13
\|
*	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \|	Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\|
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
\|
*	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \| \| \| \| \| \| \| \| \| \| \|	Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\|
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \| \| \|	In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
*	[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.