coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Allow “Let”-defined coercions	Vincent Laporte	2018-07-03
\|
*	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.
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| \| \| \| \| \|	We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
*	allow Prop as source for coercions	charguer	2018-03-09
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \|	This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
*	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \|	We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
*	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\|
*	Fixes #6129 (declaration of coercions made compatible with local definitions).	Hugo Herbelin	2017-11-14
\|
*	[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`
*	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| \| \| \|	We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
*	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\|
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|
*	[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.