coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	overlay for #6493	Enrico Tassi	2017-12-27
\|
*	[API] remove large file containing duplicate interfaces	Enrico Tassi	2017-12-27
\| \| \| \| \|	... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
*	Merge PR #6102: Fix #5998: AppVeyor package building is currently failing	Maxime Dénès	2017-12-27
\|\
\| *	Re-enable package building and artefact storage.	Maxime Dénès	2017-12-27
\| \|
\| *	Fix #5998: AppVeyor package building is currently failing	Maxime Dénès	2017-12-27
\| \|
* \|	Merge PR #6507: [ide] [doc] Document tweak to Query call.	Maxime Dénès	2017-12-27
\|\ \
* \ \	Merge PR #6504: Fix overlay selection for Circle CI.	Maxime Dénès	2017-12-27
\|\ \ \
* \ \ \	Merge PR #6040: Making coq_makefile usage consistent with what it claims + ↵	Maxime Dénès	2017-12-27
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	possibly fixing printing errors (was: Removing failure of coq_makefile on no arguments)
* \ \ \ \	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès	2017-12-27
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6444: [lib] Split auxiliary libraries into Coq-specific and general.	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6443: [vernac] Cleanup of do_definition.	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6495: Remove syntax for classification in TACTIC EXTEND.	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6494: Remove legacy Value.normalize function.	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6289: Remove unused boolean from cl_context field of ↵	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Typeclasses.typeclass
* \ \ \ \ \ \ \ \ \ \	Merge PR #6473: Fix warning about shadowing a global name.	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \|	[ide] [doc] Document tweak to Query call.	Emilio Jesus Gallego Arias	2017-12-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Fix overlay selection for Circle CI.	Gaëtan Gilbert	2017-12-26
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Delete old overlays (leaving example)	Gaëtan Gilbert	2017-12-26
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
\| \| \| \| \| \| * \| \|	[lib] Split auxiliary libraries into Coq-specific and general.	Emilio Jesus Gallego Arias	2017-12-23
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
\| \| \| \| \| \| * \|	Registering a printing handler in coq_makefile.	Hugo Herbelin	2017-12-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to fix the non-printing of error messages produced when parsing arguments.
\| \| \| \| \| \| * \|	Forbidding -o and -f in input file of coq_makefile.	Hugo Herbelin	2017-12-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was apparently either silently doing nothing or failing.
\| \| \| \| \| \| * \|	Removing failure of coq_makefile on no arguments.	Hugo Herbelin	2017-12-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Nevertheless making option -o of coq_makefile recommended as discussed in PR#6040. This is one way to resolve the inconsistency with the usage which says that all arguments are optional.
* \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \|	Remove syntax for classification in TACTIC EXTEND.	Maxime Dénès	2017-12-22
\| \|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was left ignored after 8089dc960c9e8caf778907fd87be48d77b066433.
\| \| \| \| \| \| * \| \| \|	Remove legacy Value.normalize function.	Maxime Dénès	2017-12-22
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was the identity.
* \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \|	Merge code paths in interp_definition and cleanup a bit.	Gaëtan Gilbert	2017-12-21
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	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 warning about shadowing a global name.	Gaëtan Gilbert	2017-12-19
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \|	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.