coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-22
\|\
* \	Merge PR#189: Remove tabulation support from pretty-printing.	Maxime Dénès	2017-02-20
\|\ \
\| \| *	Turning an anomaly on 'pat into a proper "unsupported" error message.	Hugo Herbelin	2017-02-09
\| \| *	Fixing an anomaly with 'pat after cofix.	Hugo Herbelin	2017-02-02
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fixing #5326 (anomaly on some unsupported case of 'pat).	Hugo Herbelin	2017-01-26
* \| \|	Adding a new evar source to remember the name of evars which were	Hugo Herbelin	2017-01-22
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-29
\| \|\ \
\| \| * \|	Fixing #5161 (case of a notation with unability to detect a recursive binder).	Hugo Herbelin	2016-10-27
* \| \| \|	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\| \| \|
\| \| * \|	Merge PR #310 into v8.5	Pierre-Marie Pédrot	2016-10-17
\| \| \|\ \
\| * \| \ \	Merge PR #310 into 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-12
\|\\| \| \| \| \|
\| \| \| \| * \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-10-12
\| * \| \| \| \|	Shorter message for "Test Asymmetric Patterns".	Hugo Herbelin	2016-10-12
\| * \| \| \| \|	Fixing a few confusions on the name of the beautify flag.	Hugo Herbelin	2016-10-12
* \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\| \| \| \| \|
\| \| \| * \| \|	Revert "Make the pretty printer resilient to incomplete nametab (progress on ...	Théo Zimmermann	2016-10-06
\| \| \| \|/ /
\| * \| \| \|	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
\| \| * \| \|	[notation] Allow to retrieve defined notations.	Emilio Jesus Gallego Arias	2016-09-25
\| \|/ / /
* \| \| \|	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