coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
\| \| \| \| \| \|	The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
*	Merge PR #6188: Rename coq-inferior.el -> inferior-coq.el to match provided ↵	Maxime Dénès	2017-11-20
\|\ \| \| \| \| \| \|	feature.
* \	Merge PR #6184: [lib] Minor pending cleanup to consolidate helper function.	Maxime Dénès	2017-11-20
\|\ \
* \ \	Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.	Maxime Dénès	2017-11-20
\|\ \ \
* \ \ \	Merge PR #6166: Fix regression in treating Defined as defined	Maxime Dénès	2017-11-20
\|\ \ \ \
* \ \ \ \	Merge PR #6163: [dev] Remove deprecation warning from `base_include`	Maxime Dénès	2017-11-20
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6161: Fix micromega.ml to match generated file and enforce match ↵	Maxime Dénès	2017-11-20
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in make.
* \ \ \ \ \ \	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵	Maxime Dénès	2017-11-20
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(clause "where" with implicit arguments)
* \ \ \ \ \ \ \	Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵	Maxime Dénès	2017-11-20
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	unbound rel
\| \| \| \| \| \| \| \| *	Rename coq-inferior.el -> inferior-coq.el to match provided feature.	Gaëtan Gilbert	2017-11-19
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #4988.
\| \| \| \| \| \| * \|	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
\| \| \| \| \| \| \| *	[lib] Minor pending cleanup to consolidate helper function.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	While we are at it we refactor a few special cases of the helper.
\| \| \| \| \| \| *	[vernac] Increase table size.	Emilio Jesus Gallego Arias	2017-11-19
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As of Nov 2017, the standard number of entries is 85, it easily goes up with some other plugins, so 211 seems like a good compromise.
* \| \| \| \| \|	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 micromega.ml to match generated file and enforce match in make.	Gaëtan Gilbert	2017-11-16
\| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Mismatch probably caused by c5aca4005.
\| \| \| \| \| \| \| \| \| *	Fix regression in treating Defined as defined	Tej Chajed	2017-11-15
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #6165.
\| \| \| \| \| \| \| \| *	[dev] Remove deprecation warning from `base_include`	Emilio Jesus Gallego Arias	2017-11-15
\| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The warning created problems as OCaml restored the color printing tags when printing it, so users doing `Drop` and then `go ()` got color printing back after the warning. We should guard the console on `Drop` better, but this requires some (much needed) refactoring work in the toplevel.
\| \| \| \| \| * \| \|	Fix gitlab for 4.06	Gaëtan Gilbert	2017-11-15
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert	2017-11-15
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
* \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	One more step in fixing #5762 ("where" clause).	Hugo Herbelin	2017-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
\| \| \| \| \| \| \| \| * \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|