coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add printers to dev/db	Gaëtan Gilbert	2017-12-22
*	Reorder dev/db	Gaëtan Gilbert	2017-12-22
*	Cleanup top_printers.mli	Gaëtan Gilbert	2017-12-22
*	Cleanup debug printers a bit, add generated mli.	Gaëtan Gilbert	2017-12-22
*	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
\|\ \ \ \
\| \| \| * \|	Compatibility of the Coq macOS package with OS X 10.11.	Théo Zimmermann	2017-12-15
\| \|_\|/ / \|/\| \| \|
\| \| * \|	Deprecate dead option Match Strict (ssr).	Gaëtan Gilbert	2017-12-14
\| \| * \|	Deprecate dead code option Congruence Depth.	Gaëtan Gilbert	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
\| \| \| \| \| \| \| \| \| * \|	Document some omega options (missing Omega Oldstyle).	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add doc for Set Debug RAKAM.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add doc for Set Debug Cbv.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add doc for Set Info/Debug Auto/Trivial/Eauto.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add optindex for Set Bullet Behavior.	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Add doc for Set Congruence Verbose	Gaëtan Gilbert	2017-12-14
\| \| \| \| \| \| \| \| \| * \|	Fix typo in doc optindex for Typeclass Resolution ...	Gaëtan Gilbert	2017-12-14
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6395: Revert [ci] Temporal workaround for checker non-backwards com...	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6388: Fix issue #6387	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #1108: [stm] Reorganize flags	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6251: [proof] Embed evar_map in RefinerError exception.	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6175: Restoring filtering of native files passed to `rm` during `ma...	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[meta] Minor linking fix.	Emilio Jesus Gallego Arias	2017-12-13
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Documenting the new options for printing "match".	Hugo Herbelin	2017-12-12
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Decompiling pattern-matching: mini-removal dead code.	Hugo Herbelin	2017-12-12
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Improving spacing in printing disjunctive patterns.	Hugo Herbelin	2017-12-12
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Revert "[ci] Temporal workaround for checker non-backwards compatible change."	Théo Zimmermann	2017-12-12
\| \|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts	Maxime Dénès	2017-12-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès	2017-12-12
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6359: Remove most uses of function extensionality in Program.Combin...	Maxime Dénès	2017-12-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6275: [summary] Allow typed projections from global state.	Maxime Dénès	2017-12-12
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \