coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
\| \| \| \| \| \| \| \| \| \| \| \|	Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
*	Merge PR #6377: Removal of the FAQ LaTex document.	Maxime Dénès	2017-12-20
\|\
* \	Merge PR #6470: Fix typo in the refman.	Maxime Dénès	2017-12-20
\|\ \
* \ \	Merge PR #6449: Let definitions must not contain side-effects when reaching ↵	Maxime Dénès	2017-12-20
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	the kernel.
* \ \ \	Merge PR #6468: Fix order of let-in representation comment.	Maxime Dénès	2017-12-20
\|\ \ \ \
* \ \ \ \	Merge PR #6471: Fix ltacprof_abstract (I think because of #6411 parallel merge).	Maxime Dénès	2017-12-20
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Fix ltacprof_abstract (I think because of #6411 parallel merge).	Gaëtan Gilbert	2017-12-19
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| \| * \|	Fix typo in the refman.	Théo Zimmermann	2017-12-19
\| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6400: Circle CI	Maxime Dénès	2017-12-19
\|\ \ \ \ \
\| \| \| * \| \|	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \|	The comment had the type and value of the let-in swapped, which contradicted the listed types.
* \| \| \| \|	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
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	an error)
* \ \ \ \ \ \ \	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 ↵	Maxime Dénès	2017-12-18
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Extraction Language command
* \ \ \ \ \ \ \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Removing the FAQ, which has been moved to the GitHub wiki for this	Matt Quinn	2017-12-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	repository. Also removing FAQ-related build rules.
* \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Fix build file	Jim	2017-12-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	For bug 6249, Segmentation fault when building Coq on Windows 10.	Jim	2017-12-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Enable builds on Windows by removing Windows-style endings where it impacts make. The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Let definitions have the same behaviour if they are ended with a Qed or a Defined command, i.e. they are treated as if they were transparent. Indeed, it doesn't make sense for them to be opaque as they are going to be expanded away at the end of the section. For an unknown reason, handling of side-effects in Let definitions considers them as if they were opaque, i.e. the effects are inlined in the definition. This discrepancy has bad consequences in the kernel, where one is forced to juggle with universe constraints generated by polymorphic Let definitions. As a first phase of cleaning, we simply enforce by typing that Let definitions should be purified before reaching the kernel. This has the intended side-effect to make side-effects persistent in Let definitions, as if they were indeed truly transparent.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[make] More build fixes for static plugins and ocamlfind.	Emilio Jesus Gallego Arias	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- In ocamlfind-based byte builds, link the VM statically as in native builds. This is the best way to get reliable, path-independent self-contained executables. - In `make install`, install the `.cmx` files for plugins too. To statically link Coq plugins in native mode, both the `.cmx` and `.o` files must be present.
\| \| \| * \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fix #5368: Canonical structure unification fails.	Pierre-Marie Pédrot	2017-12-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Universe instances were lost during constructions of the canonical instance.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Pass a ghost location for abstract	Jason Gross	2017-12-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Make [abstract] nodes show up in the Ltac profile	Jason Gross	2017-12-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This closes #5082 and closes #5778, but makes #6404 apply to `abstract` as well as `transparent_abstract`. This is unfortunate, but I think it is worth it to get `abstract` in the profile (and therefore not misassign the time spent sending the subproof to the kernel). Another alternative would have been to add a dedicated entry to `ltac_call_kind` for `TacAbstract`, but I think it's better to just deal with #6404 all at once. The "better" solution here would have been to move `abstract` out of the Ltac syntax tree and define it via `TACTIC EXTEND` like `transparent_abstract`. However, the STM relies on its ability to recognize `abstract` and `solve [ abstract ... ]` syntactically so that it can handle `par: abstract`. Note that had to add locations to `TacAbstract` nodes, as I could not figure out how to call `push_trace` otherwise.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I'm not sure if they belong in profile_ltac, or in extratactics, or, perhaps, in a separate plugin. But I'd find it very useful to have a version of `time` that works on constr evaluation, which is what this commit provides. I'm not sure that I've picked good naming conventions for the tactics, either.
\| \| \| \| \| \| \| \| \| * \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is useful for tactics that run a bunch of tests and need to display the profile for each of them.
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6386: Catch errors while coercing 'and' intro patterns	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \ \ \ \ \ \ \