coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
*	Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly	Matthieu Sozeau	2018-06-04
\|\
* \	Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.	Matthieu Sozeau	2018-06-04
\|\ \
* \| \|	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias	2018-05-31
* \| \|	Merge PR #7558: [api] Make `vernac/` self-contained.	Maxime Dénès	2018-05-30
\|\ \ \
\| \| \| *	Fix #7113: Program Let Fixpoint in section causes anomaly	Gaëtan Gilbert	2018-05-30
\| \|_\|/ \|/\| \|
\| * \|	[tactics] Turn boolean locality hint parameter into a named one.	Emilio Jesus Gallego Arias	2018-05-27
* \| \|	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\|/ /
* \|	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
\| *	Fix an anomaly when calling Obligation 0 or Obligation -1.	Théo Zimmermann	2018-05-21
* \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
* \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
* \|	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\|/
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
*	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
*	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
*	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
*	Merge PR #6275: [summary] Allow typed projections from global state.	Maxime Dénès	2017-12-12
\|\
\| *	[summary] Adapt STM to the new Summary API.	Emilio Jesus Gallego Arias	2017-12-09
* \|	Fix #6323: stronger restrict universe context vs abstract.	Gaëtan Gilbert	2017-12-06
\|/
*	Cleanup API for registering universe binders.	Matthieu Sozeau	2017-12-01
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	Restrict universe context when declaring constants in obligations.	Gaëtan Gilbert	2017-11-25
\| *	Fix obligations handling of universes anticipating stronger restrict	Matthieu Sozeau	2017-11-25
\| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| *	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\| *	Use Maps and ids for universe binders	Gaëtan Gilbert	2017-11-24
\|/
*	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
*	[api] Insert miscellaneous API deprecation back to core.	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
\| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
* \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\|/
*	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
*	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
*	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\
* \|	Statically ensuring that inlined entries out of the kernel have no effects.	Pierre-Marie Pédrot	2017-07-26
* \|	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
* \|	Merge branch 'v8.7'	Maxime Dénès	2017-07-20
\|\ \
* \| \|	Removing the uses of abstraction-breaking code in Obligations.	Pierre-Marie Pédrot	2017-07-13
\| * \|	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
* \| \|	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
\|/ /
\| *	Preparing to hints supporting discharge.	Hugo Herbelin	2017-06-27
\|/