coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\|
*	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
\|
*	Stop using Universes.subst(_opt)_univs_constr	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|	Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from?
*	Rename some universe minimizing "normalize" functions to "minimize"	Gaëtan Gilbert	2018-03-06
\| \| \| \|	UState normalize -> minimize, Evd nf_constraints -> minimize_universes
*	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
\| \| \| \| \| \|	This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
*	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \|	Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
*	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).
*	[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`
*	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.