coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Delete old overlays (leaving example)	Gaëtan Gilbert	2017-12-26
\|
*	Merge PR #6465: Gitlab touchup	Maxime Dénès	2017-12-22
\|\
* \	Merge PR #6469: No universe constraints in Let definitions	Maxime Dénès	2017-12-22
\|\ \
* \ \	Merge PR #6318: Separate vernac controls and regular commands.	Maxime Dénès	2017-12-22
\|\ \ \
* \ \ \	Merge PR #6484: Update README and CONTRIBUTING to mention the wiki and FAQ.	Maxime Dénès	2017-12-22
\|\ \ \ \
* \ \ \ \	Merge PR #6485: Fix badges.	Maxime Dénès	2017-12-22
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6445: [stm] [ide protocol] Allow to include several commands on query.	Maxime Dénès	2017-12-22
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6222: Share computation of unifiable evars	Maxime Dénès	2017-12-22
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	Fix badges.	Théo Zimmermann	2017-12-21
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| * \| \| \|	Update README and CONTRIBUTING to mention the wiki and FAQ.	Théo Zimmermann	2017-12-21
\| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6474: Fix CI with parallel make (messed up dependencies)	Maxime Dénès	2017-12-21
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Fix CI with parallel make (messed up dependencies)	Gaëtan Gilbert	2017-12-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When invoking through Makefile we always rebuild dependencies. To skip dependencies, invoke ci-wrapper directly. We make Circle CI do this. In order to properly support invoking ci-wrapper directly we replace "make" in ci-common by a bash function which adds -j to the make invocation outside submakes. We also set TIMED in the ci-wrapper.
\| \| \| \| * \| \|	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
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \|	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We force the upper layers to extrude the universe constraints before sending it to the kernel. This simplifies the suspicious handling of polymorphic constraints for section-local definitions.
* \| \| \| \| \| \| \| \|	Merge PR #6400: Circle CI	Maxime Dénès	2017-12-19
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \|	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
\| \| \| \| \| \|_\|_\|/ / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to statically ensure well-formedness properties.
\| \| \| * / \| \| \| \|	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.
\| \| \| \| \| \| \| *	Gitlab: don't ./configure in documentation job	Gaëtan Gilbert	2017-12-18
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The config/Makefile is carried over by artefacts.
* \| \| \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[stm] [ide protocol] Allow to include several commands on query.	Emilio Jesus Gallego Arias	2017-12-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a very useful feature for IDEs, as they can queue commands and display options in a single request. Change is backwards-compatible.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Overlay for unimath.	Gaëtan Gilbert	2017-12-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Do dependencies in 1 command per file class.	Gaëtan Gilbert	2017-12-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|