coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\
\| *	Disable compatibility notations warnings.	Maxime Dénès	2016-10-06
\| *	Remove the Set Verbose Compat option and turn the warning on by default.	Maxime Dénès	2016-10-06
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Fix #5048 - Casts in pattern raise an anomaly in Constrintern.	Maxime Dénès	2016-10-04
\| *	Quick fix to #4595 (making notations containing "ltac:" unused for printing).	Hugo Herbelin	2016-10-04
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Fix bug #5087: Improve the error message on record with duplicated fields.	Pierre-Marie Pédrot	2016-10-02
\| *	Warning about similar notations now up to alpha-conversion.	Hugo Herbelin	2016-09-28
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-23
\|\\|
\| *	coqc -o now places .glob file near .vo file	Enrico Tassi	2016-09-22
\| *	typos	Enrico Tassi	2016-09-22
* \|	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
* \|	Merge remote-tracking branch 'github/pr/283' into trunk	Maxime Dénès	2016-09-22
\|\ \
* \| \|	Fix an error-prone error API.	Pierre-Marie Pédrot	2016-09-21
* \| \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
\| * \|	Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.	Maxime Dénès	2016-09-20
\|/ /
\| *	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
* \|	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\ \
\| * \|	Untangling Tacexpr from lower strata.	Pierre-Marie Pédrot	2016-09-15
\| * \|	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
\| * \|	Generalizing the notion of constr substitution to generic arguments.	Pierre-Marie Pédrot	2016-09-15
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\| \|\
\| \| *	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
* \| \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \ \
* \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Notation_ops.subst_glob_vars: substituting also in evar kind for	Hugo Herbelin	2016-09-01
\| * \| \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
* \| \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\\| \| \|
* \| \| \|	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
\| * \| \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ali...	Pierre-Marie Pédrot	2016-08-23
\|/ / /
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Fix anomaly on user-inputted projection name (bug #5029).	Guillaume Melquiond	2016-08-19
\| \| *	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
\| \|/ \|/\|
\| *	Fix incorrect glob data for module symbols (bug #2336).	Guillaume Melquiond	2016-08-18
* \|	Removing dead unsafe debugging code in Constrintern.	Pierre-Marie Pédrot	2016-08-16
* \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \|	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
* \|	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin	2016-07-19
* \|	Notations with multiple recursive binders: fixing use of alpha-conversion.	Hugo Herbelin	2016-07-19
* \|	Notations: fixing multiple binders used as terms in reverse order.	Hugo Herbelin	2016-07-19
* \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
* \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
* \|	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
* \|	Fixing a bug in recognizing a recursive pattern of notations	Hugo Herbelin	2016-07-17
* \|	Fixing interpretation of notations w/ opposite instances of a recursive pattern.	Hugo Herbelin	2016-07-17