coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove branch on caml version >= 3.10 from configure.	Gaëtan Gilbert	2017-11-19
\| \| \| \|	We require 4.02.3.
*	Merge PR #6160: Fix gitlab for 4.06	Maxime Dénès	2017-11-16
\|\
* \	Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.	Maxime Dénès	2017-11-16
\|\ \
* \ \	Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵	Maxime Dénès	2017-11-16
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	local definitions)
* \ \ \	Merge PR #6104: Fixing encoding in coqdoc output tests.	Maxime Dénès	2017-11-16
\|\ \ \ \
* \ \ \ \	Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2	Maxime Dénès	2017-11-16
\|\ \ \ \ \
\| \| \| \| \| *	Fix gitlab for 4.06	Gaëtan Gilbert	2017-11-15
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #6147: Change OCAMLRUNPARAM warning to mention OCaml 4.06	Maxime Dénès	2017-11-15
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6146: coq_makefile: document COQ_SRC_SUBDIRS	Maxime Dénès	2017-11-15
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6138: Clean up/less files at root	Maxime Dénès	2017-11-15
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6122: Remove dependency of test-suite on git (fix #5725).	Maxime Dénès	2017-11-15
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6058: Remove redundant env argument to Reduction.ccnv	Maxime Dénès	2017-11-15
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6045: [travis] [coq] Complete 4.06.0 support.	Maxime Dénès	2017-11-15
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \|	Fixes #6129 (declaration of coercions made compatible with local definitions).	Hugo Herbelin	2017-11-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \|	Fixing encoding in coqdoc output tests.	Hugo Herbelin	2017-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
\| \| \| \| * \| \| \| \| \|	Move contributing files to .github/ sub-directory.	Théo Zimmermann	2017-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The overall goal is to reduce the number of files at the root of the repository.
\| \| \| \| * \| \| \| \| \|	Remove useless file README.doc.	Théo Zimmermann	2017-11-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This file is useless because all the information it contains is also in INSTALL.doc. The overall goal is to reduce the number of files at the root of the repository.
\| \| \| \| \| \| \| \| \| *	[api] Insert miscellaneous API deprecation back to core.	Emilio Jesus Gallego Arias	2017-11-13
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
\| \| \|_\|_\|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Change OCAMLRUNPARAM warning to mention OCaml 4.06	Paul Steckler	2017-11-13
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	[ci] [coq] Complete 4.06.0 support.	Emilio Jesus Gallego Arias	2017-11-13
\|/ / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Due to an API change in laglgtk, we need to update CoqIDE. We use a makefile hack so it can compile with lablgtk < 2.8.16, another option would be to require 2.8.16 as a minimal dependency. We also refactor travis to test more lablgtk versions. We also need to account for improved attribute handling in 4.06.0, in particular module aliases will propagate the deprecation status. Fixes #6140.
\| \| \| \| * / /	coq_makefile: document COQ_SRC_SUBDIRS	Enrico Tassi	2017-11-13
\| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6136: Update and simplify README.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6126: Fix ci-bignums.sh "missing ]" error.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6124: Adding a debugging printer for ident maps whose codomain ↵	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	type is unknown
* \ \ \ \ \ \ \ \ \	Merge PR #6117: Fix printing anomaly in conv	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6103: Hack to restore printing of glob_constr in debugger.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6088: Remove packaging scripts while waiting for a fix to #5998.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6071: [ci] Add Ltac2	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6065: [api] Deprecate all legacy uses of Names in core.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.	Maxime Dénès	2017-11-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Update and simplify README.	Théo Zimmermann	2017-11-10
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Fix ci-bignums.sh "missing ]" error.	Gaëtan Gilbert	2017-11-09
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It made the test always fail so ci-common was always sourced. It's not quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Adding a debugging printer for ident maps whose codomain type is unknown.	Hugo Herbelin	2017-11-08
\| \| \| \| \| \| \| \| \| \|_\|_\|_\|/ \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Actually, ocaml is apparently doing well. If there is a printer for 'a Id.Map.t and another for say Id.t Id.Map.id, it uses the most defined existing ones, so, it is apparently not a problem to have overlapping printer.
\| \| \| \| \| \| \| \| \| \| \| * \|	Remove dependency of test-suite on git (fix #5725).	Théo Zimmermann	2017-11-08
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The two lines that this commit remove are spurious as a `git clean -dfx \|\| true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`.
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6096: Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| ↵	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tac2 ]"
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6087: [feedback] Helper to print feedback messages in the console.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6086: [ci] Switch VST back to upstream.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #922: New beta-iota compatibility refinements	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fixing missing separator in an error message.	Hugo Herbelin	2017-11-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The message is the "Conversion test raised an anomaly" one.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Fixing an (apparently misplaced) spc in anomaly reporting message.	Hugo Herbelin	2017-11-08
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Hack to restore printing of glob_constr in debugger.	Hugo Herbelin	2017-11-07
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \|	[api] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias	2017-11-07
\| \|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \| \| \| \| \| \| \| \|_\|/ / / \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We do up to `Term` which is the main bulk of the changes.
\| \| \| \| \| \| \| * \| \| \| \|	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will allow to merge back `Names` with `API.Names`
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \|	Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| tac2 ]",	Samuel Gruetter	2017-11-06
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	not "first [ progress tac1 \| progress tac2 ]". And add a missing backslash.