coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \| \| \|	This API is a bit strange, I expect it will change at some point.
*	[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
\|
*	record: restore API declare_projections (removed in e414c07e1)	Enrico Tassi	2018-02-19
\|
*	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \|	We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
*	Register universe binders for record projections.	Gaëtan Gilbert	2017-11-24
\|
*	[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`
*	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+\|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j \| }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\|
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \|	It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
*	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
\|
*	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
\| \| \| \|	This is a bit long, but it is to keep a symmetry with constr_expr.
*	[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.