coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing #5454 (an assert false with 'pat).	Hugo Herbelin	2017-04-05
*	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
*	Fixing #5326 (anomaly on some unsupported case of 'pat).	Hugo Herbelin	2017-01-26
*	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
\| *	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
\|\ \ \
\| \| \| *	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
\| \| * \|	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
* \| \|	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
* \| \|	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
\|/ /
* \|	coqc -o now places .glob file near .vo file	Enrico Tassi	2016-09-22
* \|	typos	Enrico Tassi	2016-09-22
* \|	Addressing OCaml compilation warnings.	Hugo Herbelin	2016-09-16
* \|	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
* \|	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
* \|	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
\| *	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
* \|	Fixing printing of notations with several instances of a recursive pattern.	Hugo Herbelin	2016-07-17
* \|	First step in adding printing for notations such as given in #4932.	Hugo Herbelin	2016-07-17
* \|	Fixing #4932 (anomaly when using binders as terms in recursive notations).	Hugo Herbelin	2016-07-17
* \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-07-16
* \|	removing ocamldoc-related syntax errors	Matej Kosik	2016-07-12
* \|	Merge remote-tracking branch 'github/bug4653' into v8.6	Matthieu Sozeau	2016-07-07
\|\ \
\| * \|	Do not use implicit type info for (x := t) bindings	Matthieu Sozeau	2016-07-07
* \| \|	Program: fix #4873: transparency option not used	Matthieu Sozeau	2016-07-07