coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| * \|	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
* \| \| \| \|	Merge PR #6565: [Backport script] Check .mli files are not changed.	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \| \|_\|_\|/ / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6718: Fix redirection to stderr in lint-repository error message.	Maxime Dénès	2018-02-12
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6706: ci-common: guess CI_BRANCH for local builds	Maxime Dénès	2018-02-12
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| \| * \|	Merge anomaly-traces-parser.el into coqdev.el.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \|
\| \| \| \| * \|	coqdev.el: add installation instructions.	Gaëtan Gilbert	2018-02-11
\| \| \| \| \| \|
\| \| * \| \| \|	Fix redirection to stderr in lint-repository error message.	Gaëtan Gilbert	2018-02-08
\| \|/ / / / \|/\| \| \| \|
\| \| \| \| *	pre-commit: nicer messages	Gaëtan Gilbert	2018-02-08
\| \| \| \| \|
\| \| \| \| *	pre-commit: fail gracefully if fixing whitespace removes all changes	Gaëtan Gilbert	2018-02-08
\| \| \| \| \|
\| \| \| \| *	pre-commit: add files after fixing ending newlines.	Gaëtan Gilbert	2018-02-08
\| \| \| \| \|
\| \| \| \| *	Have the pre-commit hook also fix end-of-file nl	Jason Gross	2018-02-08
\| \| \| \| \|
\| \| \| \| *	Auto-create .git/hooks/pre-commit on ./configure	Jason Gross	2018-02-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files.
\| \| \| \| *	pre-commit hook: fix whitespace error detection	Gaëtan Gilbert	2018-02-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	--quiet implies --exit-code
\| \| \| \| *	A pre-commit hook to magically fix whitespace issues.	Gaëtan Gilbert	2018-02-08
\| \| \| \| \|
* \| \| \| \|	Merge PR #6610: Points to Flocq official repository.	Maxime Dénès	2018-02-07
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \ \ \ \
\| \| \| * \| \| \|	ci-common: guess CI_BRANCH for local builds	Gaëtan Gilbert	2018-02-07
\| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.	Maxime Dénès	2018-02-06
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Points to Flocq official repository.	Théo Zimmermann	2018-02-05
\| \|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
\| \| * \| \| \|	Add overlay for equations (nf_beta takes an env)	Gaëtan Gilbert	2018-02-05
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR #6654: CI: Run coqchk on Iris	Maxime Dénès	2018-02-05
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
\| \| * \| \| \|	[stm] [toplevel] Make loadpath a parameter of the document.	Emilio Jesus Gallego Arias	2018-02-05
\| \|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc...
\| * \| \| \|	CI: Run coqchk on Iris	Ralf Jung	2018-01-31
\| \| \|_\|/ \| \|/\| \|
* \| \| \|	Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵	Maxime Dénès	2018-01-31
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	menhir.
* \ \ \ \	Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.	Maxime Dénès	2018-01-31
\|\ \ \ \ \
\| \| * \| \| \|	Put default value for NJOBS in ci-common.	Gaëtan Gilbert	2018-01-30
\| \| \|/ / /
\| * \| \| \|	Adding an overlay for Equations.	Pierre-Marie Pédrot	2018-01-30
\| \| \| \| \|
* \| \| \| \|	Merge PR #6605: Safer VM interfaces	Maxime Dénès	2018-01-30
\|\ \ \ \ \
\| * \| \| \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\| \| \|/ / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.
* / \| \| \|	Use travis_retry on apt-get update	Jason Gross	2018-01-23
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration.
* \| \| \|	Merge PR #6629: Archive COMPATIBILITY	Maxime Dénès	2018-01-23
\|\ \ \ \
* \ \ \ \	Merge PR #6568: Cleanup scripts	Maxime Dénès	2018-01-23
\|\ \ \ \ \
\| \| * \| \| \|	Archive COMPATIBILITY.	Théo Zimmermann	2018-01-22
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR #6550: Remove outdated note about rlwrap in setup.txt	Maxime Dénès	2018-01-22
\|\ \ \ \ \ \ \| \|_\|/ / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6448: Cleanup and add debug printers a bit	Maxime Dénès	2018-01-18
\|\ \ \ \ \ \
\| \| \| * \| \| \|	merge-pr.sh: use git diff --quiet	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Source basic overlay before user overlays.	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Cleanup shell expansions and quoting.	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Simplify logic and streamline lint-repository.sh	Gaëtan Gilbert	2018-01-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* \| \| \| \| \| \|	Fix the wrapper around ocamldebug.	Pierre-Marie Pédrot	2018-01-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug
* \| \| \| \| \| \|	Merge PR #6483: Strong invariants in polymorphic definitions	Maxime Dénès	2018-01-12
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Adding a custom Travis overlay for HoTT.	Pierre-Marie Pédrot	2018-01-11
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #6557: First stab at documenting the test suite.	Maxime Dénès	2018-01-11
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label	Maxime Dénès	2018-01-10
\|\ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \|	[Backport script] Check .mli files are not changed.	Théo Zimmermann	2018-01-09
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Cleanup conditional in lint-repository.sh	Gaëtan Gilbert	2018-01-08
\| \| \| \| \| \|/ /
\| \| \| \| * / /	Stop talking about debian in "A note about rlwrap"	Gaëtan Gilbert	2018-01-08
\| \| \| \| \|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Debian stable version is 0.42-3 right now.
* \| \| \| \| \|	Merge PR #6549: Normalize package names	Maxime Dénès	2018-01-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6527: Update backport script for more control.	Maxime Dénès	2018-01-08
\|\ \ \ \ \ \ \
\| \| \| * \| \| \| \|	github-check-prs.py: print PR URLs when needed.	Gaëtan Gilbert	2018-01-08
\| \| \| \| \| \| \| \|