coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	github-check-prs.py: command line option to get token from a file	Gaëtan Gilbert	2018-01-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6510: Document between and exists_between types.	Maxime Dénès	2018-01-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Document between and exists_between types.	Ismail	2018-01-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06	Maxime Dénès	2018-01-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6501: Document use of ocamldebug from the command line in ↵	Maxime Dénès	2018-01-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Cygwin/Windows
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Mention -B argument of make to rerun tests	Jasper Hugunin	2018-01-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	First stab at documenting the test suite.	Jasper Hugunin	2018-01-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[PR template] Remove the relative link.	Théo Zimmermann	2018-01-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was actually pointing to https://github.com/CHANGES.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Documentation and CHANGES for bracket with goal selector.	Théo Zimmermann	2018-01-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Brackets support single numbered goal selectors.	Théo Zimmermann	2018-01-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to focus on a sub-goal other than the first one without resorting to the `Focus` command.
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Normalize MacOS installer name.	Théo Zimmermann	2018-01-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Normalize Windows installer names.	Théo Zimmermann	2018-01-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Update the lower-bound of the lablgtk dependency.	Théo Zimmermann	2018-01-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes #6509.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	update PNGs; mention async error handling; change query window to query ↵	Paul Steckler	2018-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	pane; use color descriptions
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix mli-doc issue #6531	Tony Beta Lambda	2018-01-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Ignore generated test-suite/output/MExtraction.out	Jason Gross	2017-12-31
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Trim more trailing whitespace in coq-makefile timing test	Jason Gross	2017-12-31
\| \|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces
\| \| \| \| \| \| \| * \| \| \| \| \| \|	Add a comment about universe lifting in sections in the kernel.	Pierre-Marie Pédrot	2017-12-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Expound on dependencies for github-check-prs.py	Gaëtan Gilbert	2017-12-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \|	Python script checking missing/unnecessary [needs: rebase] label	Gaëtan Gilbert	2017-12-30
\| \| \| \| \|_\|_\|_\|_\|_\|/ / / / \| \| \| \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \|	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
\| \| \| \| \| \| \| * \| \| \| \| \|	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot	2017-12-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1.
\| \| \| \| \| \| \| * \| \| \| \| \|	Hardening universe abstraction in Cooking.	Pierre-Marie Pédrot	2017-12-30
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \|	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot	2017-12-30
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Add instructions for debugging from the command line (and in Windows)	Jim Fehrle	2017-12-29
\| \| \|_\|_\|_\|_\|/ / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
\| \| \| \| \| \| \| \| \| * \|	[vernac] adds the “program” flag to the “atts” record	Vincent Laporte	2017-12-29
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	[vernac] Define types in order	Vincent Laporte	2017-12-29
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6493: [API] remove large file containing duplicate interfaces	Maxime Dénès	2017-12-29
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #975: Create checklist for pull requests.	Maxime Dénès	2017-12-29
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6492: Remove query-in-IDE warning.	Maxime Dénès	2017-12-29
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6405: Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6433: [flags] Move global time flag into an attribute.	Maxime Dénès	2017-12-29
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \|	[Makefile] plugins micromega and nsatz depend on unix and num	Vincent Laporte	2017-12-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \|	[default.nix] depends on ocamlPackages.num	Vincent Laporte	2017-12-28
\| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \|	Add TIMING_SORT_BY and --sort-by to timing scripts	Jason Gross	2017-12-27
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
\| \| \| \| \| * \| \| \| \| \| \|	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.
\| \| \| * \| \| \| \| \| \| \|	Remove query-in-IDE warning.	Maxime Dénès	2017-12-27
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL...
* \| \| \| \| \| \| \| \| \|	Merge PR #6102: Fix #5998: AppVeyor package building is currently failing	Maxime Dénès	2017-12-27
\|\ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \|	Add equations overlay.	Maxime Dénès	2017-12-27
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it.
\| * \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \