coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \
* \ \	Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.	Maxime Dénès	2017-11-13
\|\ \ \
\| \| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \|/
\| \| *	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\|
* \|	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
* \|	Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.	Maxime Dénès	2017-11-03
\|\ \
* \ \	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \ \
\| * \| \|	Do not identify a pre_ident as a string Ltac value.	Hugo Herbelin	2017-11-02
\| \| \| *	[general] Move Tactypes to `interp`	Emilio Jesus Gallego Arias	2017-11-01
\| \| \|/ \| \|/\|
\| \| *	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
* \| \|	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin	2017-10-28
\|/ /
* /	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\|/
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \|	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09
\| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
* \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\|/
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
\| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
* \|	Reporting locations in error messages about notation formats.	Hugo Herbelin	2017-09-18
\|/
*	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès	2017-09-15
\|\
* \|	Adding a missing period in a notation warning.	Hugo Herbelin	2017-09-12
* \|	Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.	Hugo Herbelin	2017-09-12
* \|	Fixing a typo in printing notations with recursive binders.	Hugo Herbelin	2017-09-12
* \|	Fixing a bug of recursive notations introduced in dfdaf4de.	Hugo Herbelin	2017-09-12
* \|	Fixing little inaccuracy in coercions to ident or name.	Hugo Herbelin	2017-09-12
\| *	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\|/
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\
* \	Merge PR #946: Functional pretyping interface	Maxime Dénès	2017-08-29
\|\ \
* \ \	Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...	Maxime Dénès	2017-08-29
\|\ \ \
* \ \ \	Merge PR #773: [flags] Remove XML output flag.	Maxime Dénès	2017-08-29
\|\ \ \ \
\| \| * \| \|	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
\| \| * \| \|	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
\| \|/ / / \|/\| \| \|
\| \| \| *	Adapting code to renaming Array.fold_map -> Array.fold_left_map.	Hugo Herbelin	2017-08-29
\| \| \| *	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
\| \|_\|/ \|/\| \|
\| * \|	[flags] Remove XML output flag.	Emilio Jesus Gallego Arias	2017-08-01
\| \| *	Remove understand_tcc_evars.	Maxime Dénès	2017-08-01
\| \|/
* /	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
\|/
*	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\
* \	Merge PR #889: Removing template polymorphism for definitions.	Maxime Dénès	2017-07-28
\|\ \
* \ \	Merge PR #888: Stronger kernel types	Maxime Dénès	2017-07-28
\|\ \ \
\| \| \| *	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| * \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\| \|/ /
* \| \|	Merge PR #894: Fixing a little location bug with recursive binders	Maxime Dénès	2017-07-26
\|\ \ \ \| \|_\|/ \|/\| \|
\| \| *	Further simplication: do not recreate entries for side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| *	Remove a horrendous hack in Declare to retrieve exported side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| *	More precise type of entries capturing their lack of side-effects.	Pierre-Marie Pédrot	2017-07-26
\| \| *	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\| \|/ \|/\|
* \|	[general] Move files to directories matching linking order.	Emilio Jesus Gallego Arias	2017-07-19