coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| * \|	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
\|\ \ \ \
* \ \ \ \	Merge PR #7745: Make type Environ.globals abstract + simplify ↵	Maxime Dénès	2018-06-29
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Environ.retroknowledge
* \ \ \ \ \	Merge PR #7950: Documentation for 8.8.1	Maxime Dénès	2018-06-29
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7860: Fix #7704: Launching coqide through PATH fails.	Emilio Jesus Gallego Arias	2018-06-28
\|\ \ \ \ \ \
\| \| * \| \| \| \|	CHANGES for 8.8.1.	Théo Zimmermann	2018-06-28
\| \| \| \| \| \| \|
\| \| * \| \| \| \|	Self-credit for the work done.	Théo Zimmermann	2018-06-28
\| \|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
* \| \| \| \| \|	Merge PR #7948: Syntax for naming an existential variable	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.	Michael Soegtrop	2018-06-28
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	wrong sphinx syntax	Ambroise	2018-06-28
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7946: Update maintainers for native/VM files in pretyping	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \|	Update gallina-extensions.rst	Ambroise	2018-06-28
\| \|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I knew this feature existed but I did not remember the syntax and I could not find it in the manual
* \| \| \| \| \| \| \|	Merge PR #7937: Mention Consortium in README	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.	Théo Zimmermann	2018-06-28
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	Deprecate Environ.retroknowledge function in favor of the projection	Gaëtan Gilbert	2018-06-28
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \|	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert	2018-06-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It's a bit shorter and more direct.
\| \| \| \| \| \| * \| \| \|	Make Environ.globals abstract.	Gaëtan Gilbert	2018-06-28
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.	Pierre-Marie Pédrot	2018-06-28
\|\ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \|	Update maintainers for native/VM files in pretyping	Maxime Dénès	2018-06-28
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7866: Implementation of mutual records in the higher strata	Maxime Dénès	2018-06-28
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7934: Add mit-plv/bedrock2-ci to CI	Emilio Jesus Gallego Arias	2018-06-28
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Add mit-plv/bedrock2-ci to CI	Andres Erbsen	2018-06-27
\|/ / / / / / / / / /
* \| \| \| \| \| \| \| \| \|	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7939: Turn the CoqProject_file module into a pure ML file	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \|	Mention Consortium in README	Maxime Dénès	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We are now actively looking for sponsors, let's make our communication more visible.
\| \| \| \| \| \| \| \| \| \| * \|	Adding overlay.	Hugo Herbelin	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \|	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms ↵	Emilio Jesus Gallego Arias	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in notations).
\| \| * \| \| \| \| \| \| \| \| \|	Slightly less crazy parsing algorithm for CoqProject_file.	Pierre-Marie Pédrot	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We use a buffer instead of O(n) appending to a string, and we also make the parser tail-call.
\| \| * \| \| \| \| \| \| \| \| \|	Turn CoqProject_file into a normal OCaml file.	Pierre-Marie Pédrot	2018-06-27
\| \|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \|	Fix 'unbound variable' issue on Windows packaging jobs.	Théo Zimmermann	2018-06-27
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \|	Test file for #7723	Maxime Dénès	2018-06-27
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	CoqIDE scrolls the proof buffer down to the first goal.	Cyprien Mangin	2018-06-27
\| \| \| \| \| \| \|_\|/ / / / \| \| \| \| \| \|/\| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Fix #7723: vm_compute segfaults with universe polymorphism	Maxime Dénès	2018-06-27
\| \| \| \| \|_\|_\|/ / / / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was revealing a critical bug in VM universe handling introduced in 8.5.
* \| \| \| \| \| \| \| \| \|	Merge PR #7888: Clarify the message "this hint will only be used by eauto"	Pierre-Marie Pédrot	2018-06-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7826: evd: restrict_evar with candidates, can raise NoCandidatesLeft	Hugo Herbelin	2018-06-26
\|\ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|