coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge code paths in interp_definition and cleanup a bit.	Gaëtan Gilbert	2017-12-21
\|
*	[vernac] Cleanup of do_definition.	Emilio Jesus Gallego Arias	2017-12-18
\| \| \| \| \|	We remove a few old-style normalization and try to use the newer APIs, however, it is hard to say whether the right magic is being used.
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is useful as it allows to reflect program_mode behavior as an attribute.
\| \| * \| \| \|	[vernac] Split `command.ml` into separate files.	Emilio Jesus Gallego Arias	2017-12-17
\| \|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Over the time, `Command` grew organically and it has become now one of the most complex files in the codebase; however, its functionality is well separated into 4 key components that have little to do with each other. We thus split the file, and also document the interfaces. Some parts of `Command` export tricky internals to use by other plugins, and it is common that plugin writers tend to get confused, so we are more explicit about these parts now. This patch depends on #6413.
\| \| \| * /	[doc] Nit on the manual.	Emilio Jesus Gallego Arias	2017-12-17
\| \|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|	`ssrnat` is mentioned, but it is not distributed with Coq.
\| \| \| *	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
\| \| \| * \| \| \| \|	Compatibility of the Coq macOS package with OS X 10.11.	Théo Zimmermann	2017-12-15
\| \|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Travis has moved on to macOS 10.12 but this makes the package incompatible with earlier versions. This fix should restore the compatibility with OS X 10.11.
\| \| * \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(fix #6106)
* \ \ \ \ \ \ \ \	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 ↵	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	same right-hand side.
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6373: Further clean-up in Reductionops, removing unused lift ↵	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	arguments.
* \ \ \ \ \ \ \ \ \ \ \ \ \	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 ↵	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	compatible change.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	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 ↵	Maxime Dénès	2017-12-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`make clean`.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[meta] Minor linking fix.	Emilio Jesus Gallego Arias	2017-12-13
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	[econstr] Small cleanup in `vernac/lemmas`	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	[econstr] Add a couple of new API functions.	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These are also convenient from `vernac` [to be used in future PRs].