coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[ci] Avoid annoying detached head warning.	Emilio Jesus Gallego Arias	2018-07-04
\|
*	Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵	Gaëtan Gilbert	2018-07-03
\|\ \| \| \| \| \| \|	with apt.
* \	Merge PR #7607: Simplify reification of predicate in bytecode and native ↵	Pierre-Marie Pédrot	2018-07-03
\|\ \ \| \| \| \| \| \| \| \| \|	compilers
* \ \	Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands	Pierre-Marie Pédrot	2018-07-03
\|\ \ \
* \ \ \	Merge PR #7942: Extend readme with 'beginners guide'	Théo Zimmermann	2018-07-03
\|\ \ \ \
* \ \ \ \	Merge PR #7974: Fix default.nix following a package renaming.	Vincent Laporte	2018-07-03
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7977: allow `make check` to succeed when -prefix is given to ↵	Emilio Jesus Gallego Arias	2018-07-03
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	./configure and make install not run yet
\| \| \| \| \| \| *	[ci] [docker] Make sure we don't install optional packages with apt.	Emilio Jesus Gallego Arias	2018-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
* \| \| \| \| \| \|	Merge PR #7703: Add an option to force parameters to be uniform	Matthieu Sozeau	2018-07-02
\|\ \ \ \ \ \ \
\| \| \| \| \| * \| \|	Add Equations overlay	Matthieu Sozeau	2018-07-02
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions	Théo Zimmermann	2018-07-02
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7965: doc: Fix typesetting in Gallina extensions	Théo Zimmermann	2018-07-02
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Clean up documentation around beginner's guide.	Siddharth Bhat	2018-07-02
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
\| \| \| \| * \| \| \|	[envars] honor env variable COQLIB	Enrico Tassi	2018-07-02
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* \| \| \| \| \| \|	Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵	Emilio Jesus Gallego Arias	2018-07-02
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	points of Camlp5
* \| \| \| \| \| \|	Merge PR #7961: [api] Fix wrong deprecation warning (#7915)	Enrico Tassi	2018-07-02
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	Adding back ocp-index to default.nix.	Théo Zimmermann	2018-07-02
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Fix default.nix following a package renaming.	Théo Zimmermann	2018-07-02
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Document option Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Add test for Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Add flag Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Implement uniform parameters in ComInductive	Jasper Hugunin	2018-07-01
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Don't allow notations attached to uniform inductives
\| * \| \| \| \|	[api] Fix wrong deprecation warning (#7915)	Emilio Jesus Gallego Arias	2018-07-01
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
* \| \| \| \|	Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	.git anymore.
* \ \ \ \ \	Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Z into three files
* \ \ \ \ \ \	Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	format).
* \ \ \ \ \ \ \	Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	break hint).
\| \| \| \| \| \| \| * \|	doc: typesetting and hyperlinks in Syntax Extensions	Lysxia	2018-06-30
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7960: [build] Remove target binary before copy.	Enrico Tassi	2018-06-30
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7949: Split the Ssrmatching module between code and grammar rules.	Enrico Tassi	2018-06-30
\|\ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Split the Ssrmatching module between code and grammar rules.	Pierre-Marie Pédrot	2018-06-30
\|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7857.
\| \| \| \| \| \| * \| \|	Adding an overlay for the PR.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Documenting the transition strategy of GEXTEND.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_tactic to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_toplevel to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_vernac to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_proofs to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_constr to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Port g_prim to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Use a homebrew parser to replace the GEXTEND extension points of Camlp5.	Pierre-Marie Pédrot	2018-06-29
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
\| \| \| \| \| \| * \|	doc: Fix typesetting in Gallina extensions	Lysxia	2018-06-29
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	Document that GITURL variables shouldn't have a trailing .git anymore.	Théo Zimmermann	2018-06-29
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows to append /archive at the end.
* \| \| \| \| \|	Merge PR #7918: Mini-update of version history with recent changes.	Théo Zimmermann	2018-06-29
\|\ \ \ \ \ \
\| \| \| \| \| * \|	Splitting primitive numeral parser/printer for positive, N, Z into three files.	Hugo Herbelin	2018-06-29
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Workaround to fix #7731 (printing not splitting line at break hint).	Hugo Herbelin	2018-06-29
\| \| \| \| \|/ / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
\| \| \| \| * \|	Fixes #7712 (an anomaly in reporting bad recursive notation format).	Hugo Herbelin	2018-06-29
\| \| \| \|/ /
* \| \| \| \|	Merge PR #7080: Swapping Context and Constr and defining declarations on ↵	Maxime Dénès	2018-06-29
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	constr in Constr
\| \| \| * \| \|	[build] Remove target binary before copy.	Emilio Jesus Gallego Arias	2018-06-29
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7666. Due to shared mapping of executables Linux doesn't allow to overwrite binaries that are running; we do as `ocamlopt` and delete the target file before copy.
* \| \| \| \|	Merge PR #7890: Inline a function from Quote used in setoid_ring.	Maxime Dénès	2018-06-29
\|\ \ \ \ \