coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| *	[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.
* \|	Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.	Maxime Dénès	2017-11-16
\|\ \
\| \| *	[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.
\| *	[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
\|/
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	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 #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
\|\ \ \ \ \
\| \| \| \| * \|	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.
* \| \| \| \|	Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.	Maxime Dénès	2017-11-08
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6086: [ci] Switch VST back to upstream.	Maxime Dénès	2017-11-08
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| * \| \| \|	[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 #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ↵	Maxime Dénès	2017-11-06
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	rules
* \ \ \	Merge PR #1139: Add a linter.	Maxime Dénès	2017-11-06
\|\ \ \ \
\| \| \| \| *	[ci] Add Ltac2	Jason Gross	2017-11-04
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #6047: A generic printer for ltac values	Maxime Dénès	2017-11-03
\|\ \ \ \
* \ \ \ \	Merge PR #6036: [toplevel] Export the last document seen after `Drop`.	Maxime Dénès	2017-11-03
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in ↵	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	dev/doc/changes.
* \ \ \ \ \ \ \	Merge PR #6024: Update of Coq version history	Maxime Dénès	2017-11-03
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík	2017-11-01
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" .
\| \| \| \| \| \| *	[ci] Switch VST back to upstream.	Théo Zimmermann	2017-10-30
\| \| \| \| \|_\|/ \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	This finally closes #5994.
\| \| \| \| * \|	[toplevel] Export the last document seen after `Drop`.	Emilio Jesus Gallego Arias	2017-10-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After `Drop`, `Coqtop.drop_last_doc` will contain the current document used by `Coqloop`. This is useful for people wanting to restart Coq after a `Drop`.
\| \| \| * \| \|	[ci] Switch back to upstream version of Math-Classes and Corn.	Théo Zimmermann	2017-10-27
\| \| \| \|/ /
\| \| * / /	Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.	Théo Zimmermann	2017-10-27
\| \| \|/ /
* \| \| \|	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\ \ \ \
* \ \ \ \	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès	2017-10-27
\|\ \ \ \ \ \| \|_\|_\|/ / \|/\| \| \| \|
\| * \| \| \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
\| \| \| * \|	Updating version history wrt 8.7.	Hugo Herbelin	2017-10-26
\| \| \| \| \|
\| \| \| * \|	Updating version history wrt 8.6.	Hugo Herbelin	2017-10-26
\| \| \| \| \|
\| \| \| * \|	Updating version history wrt 8.5.	Hugo Herbelin	2017-10-26
\| \|_\|/ / \|/\| \| \|
\| \| * \|	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\| \|/ / \| \| \| \| \| \| \| \| \| \| \| \|	To this extent we factor out the relevant bits to a new file, ltac_pretype.
\| \| *	Linter: check that files end with newlines.	Gaëtan Gilbert	2017-10-25
\| \| \| \| \| \| \| \| \| \| \| \|	We use git check-attr to look at the same files as git diff --check.
\| \| *	Put newlines at the end of files.	Gaëtan Gilbert	2017-10-25
\| \| \|
\| \| *	Add linter.	Gaëtan Gilbert	2017-10-25
\| \| \|
* \| \|	Merge PR #6003: Point HoTT back at master, which now supports Coq master	Maxime Dénès	2017-10-25
\|\ \ \
\| * \| \|	Point HoTT back at master, which now supports Coq master	Jason Gross	2017-10-23
\| \| \| \|
* \| \| \|	Switch testing branch back to CompCert upstream.	Théo Zimmermann	2017-10-20
\| \|/ / \|/\| \| \| \| \| \| \| \|	This follows the merge of AbsInt/CompCert#191.
* \| \|	Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than ↵	Maxime Dénès	2017-10-20
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	just Iris
\| * \| \|	rename ci-iris-coq -> ci-iris-lambda-rust	Ralf Jung	2017-10-19
\| \| \| \|
\| * \| \|	CI: build lambdaRust (which depends on Iris) rather than just Iris	Ralf Jung	2017-10-19
\| \|/ /
* / /	Bugzilla autolink: avoid linking inside links (fix #5974).	Gaëtan Gilbert	2017-10-18
\|/ /
* \|	Merge PR #540: [configure] Support for flambda flags.	Maxime Dénès	2017-10-10
\|\ \
* \ \	Merge PR #1067: Iris CI: use opam to install dependencies	Maxime Dénès	2017-10-10
\|\ \ \