coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.	Théo Zimmermann	2018-05-24
\|
*	Merge PR #6515: [api] Move `Vernacexpr` to parsing.	Pierre-Marie Pédrot	2018-05-24
\|\
\| *	[api] Move `Vernacexpr` to parsing.	Emilio Jesus Gallego Arias	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \|	There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more.
\| *	[api] Move `opacity_flag` to `Proof_global`.	Emilio Jesus Gallego Arias	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	`Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed.
* \|	Merge PR #7414: Add .byte targets for every bestocaml target	Enrico Tassi	2018-05-23
\|\ \ \| \|/ \|/\|
* \|	Merge PR #7567: Clean-up dead file in test-suite.	Enrico Tassi	2018-05-23
\|\ \
* \ \	Merge PR #7565: Document the new nested-proof error message.	Emilio Jesus Gallego Arias	2018-05-22
\|\ \ \
* \ \ \	Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵	Emilio Jesus Gallego Arias	2018-05-22
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	lib.cma).
\| * \| \| \|	Fixing debugger after #6859 (loading dynlink.cma before lib.cma).	Hugo Herbelin	2018-05-22
\| \| \| \| \|
* \| \| \| \|	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #7324: Infrastructure for ocamldebug on the checker	Hugo Herbelin	2018-05-22
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7526: [circle] Use Docker image from Gitlab registry.	Gaëtan Gilbert	2018-05-22
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span ↵	Gaëtan Gilbert	2018-05-22
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	multiple lines
* \ \ \ \ \ \ \	Merge PR #6859: [stm] Make toplevels standalone executables.	Théo Zimmermann	2018-05-22
\|\ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \|	[ci] [gitlab] Fix printenv sorting for variables that span multiple lines.	Emilio Jesus Gallego Arias	2018-05-21
\| \|/ / / / / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	Document the new nested-proof error message.	Théo Zimmermann	2018-05-21
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	[ide] Remove special option `-ideslave`	Emilio Jesus Gallego Arias	2018-05-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
\| * \| \| \| \| \|	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias	2018-05-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
\| * \| \| \| \| \|	[ci] Add Dune to the base system.	Emilio Jesus Gallego Arias	2018-05-21
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It is needed by Elpi and pidetop, and it is anyways needed for most OCaml packages, including some Coq tools in the future. The future base Docker image will include it by default.
* \| \| \| \| \|	Merge PR #7557: Add test cases from #7554	Théo Zimmermann	2018-05-20
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Add test cases from #7554	Tej Chajed	2018-05-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Failed in v8.7.2 but were fixed by v8.8.0.
* \| \| \| \| \| \|	Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵	Michael Soegtrop	2018-05-19
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	packaging scripts.
* \ \ \ \ \ \ \	Merge PR #7550: [CI] Fix the script used by math-classes.	Emilio Jesus Gallego Arias	2018-05-18
\|\ \ \ \ \ \ \ \ \| \|_\|/ / / / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \|	Clean-up dead file in test-suite.	Théo Zimmermann	2018-05-18
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| * \| \| \| \| \|	[CI] Fix the script used by math-classes.	Pierre-Marie Pédrot	2018-05-18
\| \|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We call configure to properly regenerate the Makefile and its dependencies.
\| \| \| \| \| * \|	Split off Universes functions for minimization.	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This finishes the splitting of Universes.
\| \| \| \| \| * \|	Make Universes.refresh_constraints internal to UState	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Split off Universes functions about substitutions and constraints	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Remove unused argument to solve_constraints_system	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Move solve_constraint_system near its only use site (comInductive)	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This API is a bit strange, I expect it will change at some point.
\| \| \| \| \| * \|	Stop using Universes.subst(_opt)_univs_constr	Gaëtan Gilbert	2018-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from?
\| \| \| \| \| * \|	Make set minimization option internal to Universes	Gaëtan Gilbert	2018-05-17
\| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| \| \| * \| \|	[circle] Use Docker image from Gitlab registry.	Emilio Jesus Gallego Arias	2018-05-17
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵	Emilio Jesus Gallego Arias	2018-05-17
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	by default.
* \ \ \ \ \	Merge PR #7359: Reduce usage of evar_map references	Pierre-Marie Pédrot	2018-05-17
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵	Pierre-Marie Pédrot	2018-05-17
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`comDefinition`.
* \ \ \ \ \ \ \	Merge PR #6870: [ide] Don't set `quiet` on start.	Enrico Tassi	2018-05-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7525: [ci] Try to build more of fiat-crypto.	Gaëtan Gilbert	2018-05-17
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6808: Add unit tests to test-suite	Gaëtan Gilbert	2018-05-17
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \|	Document nested proofs and associated option.	Théo Zimmermann	2018-05-17
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \|	[STM] Nested Proofs Allowed has to be executed immediately	Enrico Tassi	2018-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	since it affects scheduling (actually the error the option lets one silence)
\| \| \| \| \| \| * \| \| \| \|	Remove deprecation warning for nested proofs.	Théo Zimmermann	2018-05-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It is not clear yet that support for nested proofs will actually get removed in a future version.
\| \| \| \| \| \| * \| \| \| \|	Introduce an option to allow nested lemma, and turn it off by default.	Théo Zimmermann	2018-05-17
\| \|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.	Maxime Dénès	2018-05-16
\|\ \ \ \ \ \ \ \ \ \
\| \| * \| \| \| \| \| \| \| \|	Modify make system to include Makefile.common in the test suite	Gaëtan Gilbert	2018-05-16
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	[ci] Try to build more of fiat-crypto.	Emilio Jesus Gallego Arias	2018-05-16
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #7514: [ci] Don't build lite versions of CI developments.	Gaëtan Gilbert	2018-05-16
\|\ \ \ \ \ \ \ \ \ \