coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09
*	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
\| *	Fixing a little location bug with recursive binders.	Hugo Herbelin	2017-07-18
* \|	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\|\
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| *	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \|\
* \| \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \
* \ \ \	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \ \
* \ \ \ \	Merge PR#765: Remove obsolete Show commands	Maxime Dénès	2017-06-14
\|\ \ \ \ \
* \| \| \| \| \|	[print] Allow Selective Printing of Notations	Emilio Jesus Gallego Arias	2017-06-14
\| \| \| * \| \|	Notation.declare_rawnumeral_interpreter	Pierre Letouzey	2017-06-14
\| \| \| * \| \|	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| \|_\|/ / / \|/\| \| \| \|
\| \| * \| \|	Remove support for Coq 8.2.	Guillaume Melquiond	2017-06-14
\| \|/ / / \|/\| \| \|
\| * \| \|	Remove more dead code (follow-up of previous commit).	Théo Zimmermann	2017-06-12
\|/ / /
\| * \|	Fix Bug #5568, no dup notation warnings on repeated module imports	Paul Steckler	2017-06-09
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\\| \|