coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #1150: [stm] Remove all but one use of VtUnknown.	Maxime Dénès	2017-12-11
\|\
* \	Merge PR #6338: Remove up-to-conversion term matching	Maxime Dénès	2017-12-11
\|\ \
* \ \	Merge PR #6369: [api] Remove kernel dependency on intf (Decl_kind)	Maxime Dénès	2017-12-11
\|\ \ \
* \ \ \	Merge PR #6363: [META] Some dependency fixes.	Maxime Dénès	2017-12-11
\|\ \ \ \
* \ \ \ \	Merge PR #6358: [ci] Download ci-sf archives into the proper CI build dir.	Maxime Dénès	2017-12-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6351: Fix a copy-paste error in ci-ltac2.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6346: [ci] CoLoR has moved to github	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6340: [default.nix] Add ocpIndent and ocp-index.	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6370: [ci] Temporal workaround for checker non-backwards ↵	Maxime Dénès	2017-12-10
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	compatible change.
\| * \| \| \| \| \| \| \| \|	[ci] Temporal workaround for checker non-backwards compatible change.	Emilio Jesus Gallego Arias	2017-12-10
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| \| \|_\|_\|_\|_\|/ / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
\| \| \| \| \| \| * \| \|	[META] Some dependency fixes.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|/ / / \| \|/\| \| \| \| \| \|
\| \| \| \| \| \| \| *	[stm] Remove all but one use of VtUnknown.	Emilio Jesus Gallego Arias	2017-12-09
\| \| \|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Together with #1122, this makes `VernacInstance` the only command in the Coq codebase that cannot be statically determined to open a proof. The reasoning for the commands moved to `VtSideff` is that parser-altering commands should be always marked `VtNow`; the rest can be usually marked as `VtLater`.
\| \| \| \| \| \| *	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	They were not used anymore since the previous patches.
\| \| \| \| \| * \|	[ci] Download ci-sf archives into the proper CI build dir.	Emilio Jesus Gallego Arias	2017-12-09
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Currently, `make ci-sf` downloads and builds the files in the main root directory. we fix that.
\| * \| \| \| \|	Revert "CI: poc Circleci configuration"	Arnaud Spiwack	2017-12-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34.
\| * \| \| \| \|	CI: poc Circleci configuration	Arnaud Spiwack	2017-12-08
\|/ / / / /
\| \| \| * \|	Fix a copy-paste error in ci-ltac2.	Théo Zimmermann	2017-12-08
\| \| \| \| \|
* \| \| \| \|	Merge PR #6334: Remove dead code in Reductionops	Maxime Dénès	2017-12-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6158: Allows a level in the raw and glob printers	Maxime Dénès	2017-12-08
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6224: Add alienclean target to remove compilation products with no ↵	Maxime Dénès	2017-12-08
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	source.
\| \| \| \| \| * \| \|	[ci] CoLoR has moved to github	Emilio Jesus Gallego Arias	2017-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes #6194 .
* \| \| \| \| \| \| \|	Merge PR #6267: Fix PR merge script.	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	[default.nix] Add ocpIndent and ocp-index.	Maxime Dénès	2017-12-07
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Getting rid of pf_matches in Hipattern.	Pierre-Marie Pédrot	2017-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Funnily enough, the old code is completely bogus. It succeeds in early files of the prelude just because the heterogeneous equality has not been required. This raises an exception which is not the same one as if we tried to rewrite with the identity type first. The only user, the inversion tactic, was actually only relying on Logic.eq and was furthermore not even using the convertibility algorithm. We just perform a syntactic match now.
* \| \| \| \| \| \| \|	Merge PR #6290: Rename update to set, Fixes #6196	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #873: New strategy based on open scopes for deciding which notation ↵	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to use among several of them
* \ \ \ \ \ \ \ \ \	Merge PR #6142: Single quotes break on Windows	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6277: Qualified import in coqchk	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding)	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6321: Use preference for ocamlfind in configure	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6316: Correct typo	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6309: [default.nix] needs ncurses for the test-suite	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6303: Remove redundant Zcase from the checker.	Maxime Dénès	2017-12-07
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Getting rid of pf_is_matching in Funind.	Pierre-Marie Pédrot	2017-12-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was dead code, probably due to the fact it was once shared with the kernel stack type.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was actually not used. The only place generating one was easily writable without it.
\| \| \| \| \| * \| \| \| \| \| \| \| \|	Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.	Hugo Herbelin	2017-12-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes #6286 as suggested by PMP. See details of discussion at #6286.
\| \| \| \| \| \| \| \| \| * \| \| \| \|	Rename update to set, fixes #6196	Paul Steckler	2017-12-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \|	use preference for ocamlfind	Paul Steckler	2017-12-05
\| \|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \| \| \|	Correct typo	Martin Vassor	2017-12-05
\| \|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \|	[default.nix] explain ncurses dependency	Vincent Laporte	2017-12-05
\| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #890: Global universe declarations	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6266: Safe unmarshalling in the checker	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6301: [vernac] Couple of tweaks missing from previous PRs.	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6306: Adding a test for #6304 (a bug with "fix" in notations).	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6300: Clarify operation of sequences, fixes #6095	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6293: Check for Num lib if OCaml >= 4.06, fixes #6162	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007	Maxime Dénès	2017-12-05
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \