coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix an outdated comment refering to lib/dnet.mli	Armaël Guéneau	2018-05-30
\|
*	Merge PR #7419: Remove 100 occurrences of Evd.empty	Pierre-Marie Pédrot	2018-05-28
\|\
* \	Merge PR #7573: Remove unused Printer.printer_pr override mechanism.	Hugo Herbelin	2018-05-27
\|\ \
* \ \	Merge PR #7543: [ide] Move common protocol library to its own folder/object.	Pierre-Marie Pédrot	2018-05-26
\|\ \ \
* \ \ \	Merge PR #7603: Use -j 1 for high memory fiat crypto targets	Emilio Jesus Gallego Arias	2018-05-26
\|\ \ \ \
* \ \ \ \	Merge PR #7285: Give advice on managing GitHub notifications in CONTRIBUTING.	Maxime Dénès	2018-05-26
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6057: Start a release process documentation.	Maxime Dénès	2018-05-26
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge pull request #7569 from ppedrot/clean-newring	Assia Mahboubi	2018-05-25
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Simplify the newring hack
* \ \ \ \ \ \ \	Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was added	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7467: Remove unused references from biblio.	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7551: Update CODEOWNERS (mostly regarding the test-suite)	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	Change primary maintainer for the checker.	Théo Zimmermann	2018-05-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Primary maintainers should be responsive. [ci skip]
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7556: Add a setting to warn about empty object in the refman	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| *	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We address the easy ones, but they should probably be all removed.
\| \| \| \| \| \| \| \| * \| \|	Use -j 1 for high memory fiat crypto targets	Gaëtan Gilbert	2018-05-25
\| \|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #7508: Improve rewrite section in tactic chapter.	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7533: [sphinx] Bump timeout. Closes #7532.	Maxime Dénès	2018-05-25
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7196: [tactics] Remove anonymous fix/cofix form.	Pierre-Marie Pédrot	2018-05-25
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵	Pierre-Marie Pédrot	2018-05-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	global env
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7598: Fix recipe for FAKEIDEBYTE	Enrico Tassi	2018-05-25
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[tactics] Remove anonymous fix/cofix form.	Emilio Jesus Gallego Arias	2018-05-24
\| \|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer.
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix recipe for FAKEIDEBYTE	Gaëtan Gilbert	2018-05-24
\|/ / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Caused by a semantic conflict with the separate toplevels PR.
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7574: Improve merging and overlay documentations.	Emilio Jesus Gallego Arias	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Remove the unused printer_pr mechanism.	Jim Fehrle	2018-05-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \|	Complete rewrite of the documentation of overlays after Jim's additional ↵	Théo Zimmermann	2018-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	comments. [ci skip]
\| * \| \| \| \| \| \| \| \| \| \| \|	Relax advice on the name of user-overlays following Gaëtan's suggestion.	Théo Zimmermann	2018-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci skip]
\| * \| \| \| \| \| \| \| \| \| \| \|	Improve merging and overlay documentations.	Théo Zimmermann	2018-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Clarification prompted by Jim Fehrle. [ci skip]
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in CArray
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7594: Fix #5983 (many frequent AppVeyor failures) by increasing ↵	Emilio Jesus Gallego Arias	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	spawn timeout.
\| \| \| * \| \| \| \| \| \| \| \| \| \|	Fix #7323: coqchk puts polymorphic univs of inductive in global env	Gaëtan Gilbert	2018-05-24
\| \|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| *	[ide] Move common protocol library to its own folder/object.	Emilio Jesus Gallego Arias	2018-05-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7581: Mention warning and error message docs in PR template	Théo Zimmermann	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	instances
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.	Enrico Tassi	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.	Théo Zimmermann	2018-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7582: [ci] Build fiat-crypto targets in sequence	Emilio Jesus Gallego Arias	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6515: [api] Move `Vernacexpr` to parsing.	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Document Smart/Array changes in dev/doc/Changes.md.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Renaming miscellaneous internal smart functions.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Collecting Map.smart_* functions into a module Map.Smart.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Moving Rtree.smart_map into Rtree.Smart.map.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.	Hugo Herbelin	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This follows the model of smartmap and smartmap2.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	CArray: adding combinators.	Hugo Herbelin	2018-05-23
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Fix #7576: broken link for Delahaye paper.	Théo Zimmermann	2018-05-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Remove unused references from biblio.	Théo Zimmermann	2018-05-23
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|