coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\
\| *	Merge PR #289 into v8.6.	Pierre-Marie Pédrot	2016-10-12
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \|
\| * \|	Warning about similar notations now up to alpha-conversion.	Hugo Herbelin	2016-09-28
\| \| *	[notation] Allow to retrieve defined notations.	Emilio Jesus Gallego Arias	2016-09-25
\| \|/
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
* \| \|	Changing the definition of the "Lib.variable.info" type to enable us to do mo...	Matej Kosik	2016-08-24
\| \|/ \|/\|
\| *	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
\| *	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\| *	Unify location handling of error functions.	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Fixing #4865 (deciding on which arguments to recompute scopes was not robust).	Hugo Herbelin	2016-06-29
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Properly handling the only printing flag when parsing rules already exist.	Pierre-Marie Pédrot	2016-06-28
*	Removing the use to Egramcoq.recover_constr_grammar.	Pierre-Marie Pédrot	2016-06-07
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Revert "A heuristic to add parentheses in the presence of rules such as"	Hugo Herbelin	2016-04-27
*	A heuristic to add parentheses in the presence of rules such as	Hugo Herbelin	2016-04-27
*	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\
* \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \
\| * \|	Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.	Pierre-Marie Pédrot	2016-03-03
* \| \|	Printing notations: Cleaning in anticipation of fixing #4592.	Hugo Herbelin	2016-02-28
\|/ /
* \|	Update copyright headers.	Maxime Dénès	2016-01-20
\| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\|/
*	Make sure that scope classes are displayed by Print Scopes. (Fix bug #4262)	Guillaume Melquiond	2015-07-08
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Normalize scope names before storing them in vo files. (Fix for bug #4162)	Guillaume Melquiond	2015-03-27
*	Fixing equality of notation_constrs. Fixes bug #4136.	Pierre-Marie Pédrot	2015-03-24
*	Revert "Useless check when loading notations through import."	Pierre-Marie Pédrot	2015-03-24
*	Update headers.	Maxime Dénès	2015-01-12
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Fix HoTT bug #84, binding scopes to projections.	Matthieu Sozeau	2014-06-17
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing generic hashes and replacing them with proper ones.	Pierre-Marie Pédrot	2014-03-03
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Fixing pervasive comparisons	Pierre-Marie Pédrot	2014-03-01
*	Useless check when loading notations through import.	Pierre-Marie Pédrot	2014-03-01
*	Reverting the old LIFO behaviour of the notation finding algorithm.	ppedrot	2013-11-08
*	Do not generate useless argument arrays in whd_* functions.	ppedrot	2013-10-29
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Some more hand-written comparison functions to avoid polymorphic comparison.	xclerc	2013-10-14