coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of ↵	Pierre-Marie Pédrot	2018-04-01
\|\ \| \| \| \| \| \|	tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable
* \	Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)	Pierre-Marie Pédrot	2018-04-01
\|\ \
* \ \	Merge PR #7132: [doc] Add some more documentation to STM API.	Enrico Tassi	2018-04-01
\|\ \ \
* \ \ \	Merge PR #6802: Remove deprecated commands Implicit Arguments and Arguments ↵	Enrico Tassi	2018-04-01
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Scope
\| \| * \| \|	[doc] Add some more documentation to STM API.	Emilio Jesus Gallego Arias	2018-03-31
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \
\| \| * \| \|	Add CHANGES for removing Implicit Arguments and Arguments Scope	Jasper Hugunin	2018-03-30
\| \| \| \| \|
\| \| * \| \|	Remove deprecated commands Arguments Scope and Implicit Arguments	Jasper Hugunin	2018-03-30
\| \| \| \| \|
\| \| * \| \|	Change Implicit Arguments to Arguments in test-suite	Jasper Hugunin	2018-03-30
\| \|/ / / \|/\| \| \|
* \| \| \|	Merge PR #7121: Remove outdated patch from ci-sf	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \
* \ \ \ \	Merge PR #6989: Enable whitespace checking for new Sphinx file extensions.	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7111: Fix #6631: Derive Plugin gives "Anomaly: more than one ↵	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	statement".
\| \| \| \| * \| \|	Linter: verify overlay extensions.	Gaëtan Gilbert	2018-03-31
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	pre-commit: verify user overlay extensions (must be .sh).	Gaëtan Gilbert	2018-03-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This has come up a couple times.
* \| \| \| \| \| \|	Merge PR #7130: gitlab: fix environment for build template	Emilio Jesus Gallego Arias	2018-03-31
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	gitlab: fix environment for build template	Gaëtan Gilbert	2018-03-30
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When `build` was made to build the doc it dropped `-coqide opt` and dropped the environment variables for building coqide. The combination means that when the cache had lablgtk in opam (installed by some other job) configure would pick it up but the system package wouldn't be there causing a failure. When lablgtk isn't in the cache everything was fine.
\| \| \| * / /	Remove outdated patch from ci-sf	Jasper Hugunin	2018-03-29
\| \|_\|/ / / \|/\| \| \| \|
\| * \| \| \|	Fix #6631: Derive Plugin gives "Anomaly: more than one statement".	Pierre-Marie Pédrot	2018-03-29
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We use a lower level function that accesses the proof without raising an anomaly. This is a direct candidate for backport, so I used a V82 API but eventually this API should be cleaned up.
* \| \| \|	Merge PR #7057: Sphinx Chapter 20: Type Classes	Maxime Dénès	2018-03-29
\|\ \ \ \
* \ \ \ \	Merge PR #7072: Update codeowners	Maxime Dénès	2018-03-29
\|\ \ \ \ \
\| * \| \| \| \|	Remove dev/doc/changes.md from files with a code owner.	Théo Zimmermann	2018-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Like CHANGES, and the test-suite folder, this file receives too many updates to have a code owner. It is the job of the reviewer of the PR to review changes to these files as well.
\| \| \| \| * \|	Supporting fix/cofix in Ltac pattern-matching (wish #7092).	Hugo Herbelin	2018-03-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern.
\| \| \| \| * \|	Patterns: Accepting patterns in PFix and PCofix and not only constr.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
\| \| \| \| * \|	Adding Array.fold_left4.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
\| \| \| \| * \|	Detyping: Adding a variant of share_names for patterns.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
\| \| \| \| * \|	Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
\| \| \| \| * \|	Patternops: renaming an internal function to more closely match its effect.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
\| \| \| \| * \|	Glob_ops: cosmetic renaming to reflect the type of objects.	Hugo Herbelin	2018-03-28
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR #7090: stm: don't propagate side effects when editing a proof	Emilio Jesus Gallego Arias	2018-03-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6961: [test-suite] Add backtracking test for `Load`.	Enrico Tassi	2018-03-28
\|\ \ \ \ \ \ \
\| \| * \| \| \| \| \|	stm: don't propagate side effects when editing a proof	Enrico Tassi	2018-03-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Adding tacticals tclBINDFIRST/tclBINDLAST.	Hugo Herbelin	2018-03-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Design choice: Failing with an anomaly or with a catchable Ltac error "Fail": we fail with a Fail as it was the case with the related constrained version of tclTHENFIRST/tclTHENLAST.
\| \| \| \| \| \| \| *	Export Proofview.undefined as "unsafe" primitive.	Hugo Herbelin	2018-03-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Adding informative variant of shelve_unifiable returning set of shelved evars.	Hugo Herbelin	2018-03-27
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *"	Pierre-Marie Pédrot	2018-03-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7062: Slightly refining some error messages about unresolvable evars.	Pierre-Marie Pédrot	2018-03-27
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	[doc] Port Chapter 20 Type Classes to Sphinx	Matthieu Sozeau	2018-03-26
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes ↵	Maxime Dénès	2018-03-26
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	AppVeyor fail.
\| \| \| \| \| \| * \| \|	Move Classes.tex to type-classes.rst	Matthieu Sozeau	2018-03-26
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.	Enrico Tassi	2018-03-26
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Add Michael Soegtrop as a code owner for Windows build scripts.	Théo Zimmermann	2018-03-26
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Use Pierre Corbineau GitHub nickname in CODEOWNERS.	Théo Zimmermann	2018-03-26
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Slightly refining some error messages about unresolvable evars.	Hugo Herbelin	2018-03-24
\| \|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For instance, error in "Goal forall a f, f a = 0" is now located.
\| \| \| * \| \| \|	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
\| \|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- The case 0 makes the code of intros until (and in particular of Detyping.lookup_quantified_hypothesis_as_displayed more complicated). - The introduction pattern "*" is compositional while "until 0" is not.
* \| \| \| \| \|	Merge PR #7046: Switch maintainers for documentation	Théo Zimmermann	2018-03-23
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7018: Fix typo in CHANGES.	Maxime Dénès	2018-03-23
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7029: improve merge-pr script	Maxime Dénès	2018-03-23
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	improve merge-pr script	Enrico Tassi	2018-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The script now performs many more checks and reports errors in a more intelligible way.
* \| \| \| \| \| \| \| \|	Merge PR #7052: More precise wording about the merge process.	Théo Zimmermann	2018-03-23
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	More precise wording about the merge process.	Maxime Dénès	2018-03-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, don't use the GitHub interface. Also, not all reviews are mandatory in some corner cases.