coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
*	Merge PR #6436: Fix #5368: Canonical structure unification fails.	Maxime Dénès	2017-12-18
\|\
* \	Merge PR #6447: [make] More build fixes for static plugins and ocamlfind.	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6284: Warning for absolute name masking (deprecated, should become ...	Maxime Dénès	2017-12-18
\|\ \ \
* \ \ \	Merge PR #6381: A version of [time] that works on constr evaluation	Maxime Dénès	2017-12-18
\|\ \ \ \
* \ \ \ \	Merge PR #6406: Make [abstract] nodes show up in the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6380: Add tactics to reset and display the Ltac profile	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6305: Build with windows line endings	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6217: Do dependencies in 1 command per file class.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6453: [doc] Nit on the manual.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6411: Fix #5081 by more fine-grained LtacProf recording	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6419: [vernac] Split `command.ml` into separate files.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \| \| \| \|	[flags] Make program_mode a parameter for commands in vernac.	Emilio Jesus Gallego Arias	2017-12-17
\| \| * \| \| \| \| \| \| \| \| \| \| \|	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/ / / / / / / / / / / /
\| \| \| * / / / / / / / / /	[doc] Nit on the manual.	Emilio Jesus Gallego Arias	2017-12-17
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \|	Fix build file	Jim	2017-12-16
\| \| \| \| * \| \| \| \| \| \| \|	For bug 6249, Segmentation fault when building Coq on Windows 10.	Jim	2017-12-16
\| \| \| \| \| \| \| \| \| \| * \|	[make] More build fixes for static plugins and ocamlfind.	Emilio Jesus Gallego Arias	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Overlay for unimath.	Gaëtan Gilbert	2017-12-15
\| \| \| * \| \| \| \| \| \| \|	Do dependencies in 1 command per file class.	Gaëtan Gilbert	2017-12-15
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11.	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6219: Document undocumented options	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6429: 8.7.1 CHANGES.	Maxime Dénès	2017-12-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[econstr] Switch constrintern API to non-imperative style.	Emilio Jesus Gallego Arias	2017-12-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix #5368: Canonical structure unification fails.	Pierre-Marie Pédrot	2017-12-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Compatibility of the Coq macOS package with OS X 10.11.	Théo Zimmermann	2017-12-15
\| \|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \|	Pass a ghost location for abstract	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| \| * \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Add documentation for time_constr	Jason Gross	2017-12-14
\| \| * \| \| \| \| \| \| \| \| \|	Deprecate dead option Match Strict (ssr).	Gaëtan Gilbert	2017-12-14
\| \| * \| \| \| \| \| \| \| \| \|	Deprecate dead code option Congruence Depth.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| \| * \|	Add named timers to LtacProf	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| \|/ /
\| \| \| \| \| \| \| \| \| * \|	Add doc+changelog entries for new LtacProf tactics	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add tactics to reset and display the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6379: Fix profiling plugin	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6422: [meta] Minor linking fix.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	8.7.1 CHANGES.	Théo Zimmermann	2017-12-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Document Short Module Printing.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Document Rewriting Schemes (quickly).	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Document Record Elimination Schemes.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Document Asymmetric Patterns.	Gaëtan Gilbert	2017-12-14