coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
*	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
*	Being defensive in printing implicit arguments also with manual	Hugo Herbelin	2016-06-16
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-09
\|\
\| *	Fix bug #4777: Printing time is impacted by large terms that don't print.	Pierre-Marie Pédrot	2016-06-07
* \|	A slight phase of documentation and uniformization of names of	Hugo Herbelin	2016-06-02
* \|	Revert "Being defensive in printing implicit arguments also with manual"	Hugo Herbelin	2016-04-27
* \|	Being defensive in printing implicit arguments also with manual	Hugo Herbelin	2016-04-27
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \| \|	A more explicit name to the asymmetric boolean flag.	Hugo Herbelin	2016-03-12
* \| \|	merging conflicts with the original "trunk__CLEANUP__Context__2" branch	Matej Kosik	2016-02-15
\|\ \ \
* \ \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-13
\|\ \ \ \ \| \| \|_\|/ \| \|/\| \|
\| * \| \|	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
\| \| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
\|/ /
* \|	Fix a bug in externalisation which prevented printing of projections	Matthieu Sozeau	2015-12-02
* \|	Make the pretty printer resilient to incomplete nametab (progress on #4363).	Enrico Tassi	2015-11-26
\| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\|/
*	Continuing experimentation on what part of the instance of an evar	Hugo Herbelin	2015-02-21
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Reactivating option "Set Printing Existential Instances" for asking printing ...	Hugo Herbelin	2014-12-04
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	More on printing references applied to implicit arguments.	Hugo Herbelin	2014-09-16
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Fix bug #3591: print differently eta-expanded projection implicit application...	Matthieu Sozeau	2014-09-08
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Spotted a source of failure of the constr printer in debugger.	Hugo Herbelin	2014-08-18
*	Fix non-printing of coercions for primitive projections (fixes bug #3433).	Matthieu Sozeau	2014-08-14
*	Change internalization of primitive projections to allow parsing [p t] as	Matthieu Sozeau	2014-08-08
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Consistent pretty-printing of primitive projections and their expanded forms.	Matthieu Sozeau	2014-07-31
*	Fix printing of projections with implicits.	Matthieu Sozeau	2014-05-06