coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixes #7195 (missing freshness condition in Ltac pattern-matching names).	Hugo Herbelin	2018-04-08
\| \| \| \| \| \| \| \| \| \|	We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix.
*	Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not ↵	Hugo Herbelin	2018-04-06
\|\ \| \| \| \| \| \|	provide line number
* \	Merge PR #6960: [api] Move some types to their proper module.	Pierre-Marie Pédrot	2018-04-06
\|\ \
* \ \	Merge PR #7180: Remove unused script.	Pierre-Marie Pédrot	2018-04-06
\|\ \ \
* \ \ \	Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)	Enrico Tassi	2018-04-06
\|\ \ \ \
* \ \ \ \	Merge PR #7131: Sphinx doc chapter 30	Théo Zimmermann	2018-04-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6838: Light refactoring of implicit arguments	Hugo Herbelin	2018-04-05
\|\ \ \ \ \ \
* \| \| \| \| \| \|	Refactor impargs code.	Jasper Hugunin	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should preserve semantics exactly. In the compute_implicits family of functions, I changed the name of the pushed rel to not be fresh, but the env isn't passed to find_displayed_name_in, and shouldn't affect whd_all.
\| \| \| \| * \| \|	Remove unused script.	Théo Zimmermann	2018-04-05
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is dead code since fd44a40f9d426a7b65f167bc30d320a0f7dd2bbd. This script was initially introduced in a088d03434417e935df3c75f81a954eadbdfc2b8 and left untouched since then.
\| \| \| \| \| *	Fix #7124: Warning "Ignoring implicit status" does not provide line number	Maxime Dénès	2018-04-05
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	Fixes issue #7172 (don't include MinGW make in install)	Michael Soegtrop	2018-04-05
\| \| \| \| \|
* \| \| \| \|	Merge PR #7169: Sphinx docs: fix typo in Chrząszcz (non-ASCII character ↵	Maxime Dénès	2018-04-05
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	lost in sphinx migration)
* \ \ \ \ \	Merge PR #7074: Update merging doc	Maxime Dénès	2018-04-05
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \|
\| * \| \| \| \|	Add note for homebrew users.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \|
\| * \| \| \| \|	Some advice about merge script dependencies.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Including: how to create a GPG key.
\| * \| \| \| \|	Improve the MERGING doc.	Théo Zimmermann	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, describes what to do with overlays.
\| * \| \| \| \|	Adapt CONTRIBUTING to recent changes in Coq.	Théo Zimmermann	2018-04-05
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- The testing and benchmarking labels are now distinct. - The release manager does not take care of merging anymore. - The reference manual is not written in LaTeX anymore.
* \| \| \| \|	Merge PR #7115: Sphinx doc chapter 28	Théo Zimmermann	2018-04-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"	Enrico Tassi	2018-04-05
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	[Sphinx] Add chapter 30	Maxime Dénès	2018-04-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Paul Steckler for porting this chapter.
\| \| \| \| \| \| * \|	[Sphinx] Move chapter 30 to new infrastructure	Maxime Dénès	2018-04-05
\| \| \| \| \|_\|/ / \| \| \| \|/\| \| \|
* \| \| \| \| \| \|	Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.	Hugo Herbelin	2018-04-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7163: merge-pr.sh: cache github API calls	Maxime Dénès	2018-04-04
\|\ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \|	Sphinx docs: fix typo (non-ASCII character lost in sphinx migration)	Peter LeFanu Lumsdaine	2018-04-04
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| * \| \|	[Sphinx] Add chapter 28	Maxime Dénès	2018-04-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Paul Steckler for porting this chapter.
\| \| \| \| \| * \| \|	[Sphinx] Move chapter 28 to new infrastructure	Maxime Dénès	2018-04-04
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7158: [meta] Add `num` to the set of base libraries.	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6407: Fix #6404 - Print tactics called by ML tactics	Pierre-Marie Pédrot	2018-04-04
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7147: [doc] Document better ocamlfind and flambda requirements.	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps ↵	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with #7142]
* \ \ \ \ \ \ \ \ \ \	Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.	Enrico Tassi	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7104: Sphinx doc chapter 27	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7048: Sphinx doc chapter 25	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7049: Sphinx doc chapter 26	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7047: Sphinx doc chapter 24	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7041: Sphinx doc chapter 23	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7037: Sphinx doc chapter 18	Théo Zimmermann	2018-04-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	merge-pr.sh: cache github API calls	Gaëtan Gilbert	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7154: Update coq_makefile timing test	Gaëtan Gilbert	2018-04-03
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[doc] Document better ocamlfind and flambda requirements.	Emilio Jesus Gallego Arias	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Closes #6782
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	[meta] Add `num` to the set of base libraries.	Emilio Jesus Gallego Arias	2018-04-03
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In the META file, the set of base libraries is determined by the dependencies of the `coq.clib` package. We add `num` to the dependencies as otherwise dynamically loading `micromega` and `nsatz` will fail as they require the toplevel to have `num` linked in.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update coq_makefile timing test	Jason Gross	2018-04-02
\|/ / / / / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes #5675 (in yet another way). The issue was that `$` (end of string regex) was not properly escaped in `"`s. This handles the issue that is displayed in ``` cat A.v.timing.diff After \| Code \| Before \|\| Change \| % Change --------------------------------------------------------------------------------------------------- 0m01.44s \| Total \| 0m01.56s \|\| -0m00.12s \| -7.92% --------------------------------------------------------------------------------------------------- 0m00.609s \| Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] \| 0m00.627s \|\| -0m00.01s \| -2.87% 0m00.527s \| Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] \| 0m00.552s \|\| -0m00.02s \| -4.52% 0m00.304s \| Chars 000 - 026 [Require~Coq.ZArith.BinInt.] \| 0m00.379s \|\| -0m00.07s \| -19.78% N/A \| Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] \| 0m00.006s \|\| -0m00.00s \| -100.00% 0m00.s \| Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] \| N/A \|\| +0m00.00s \| N/A --- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000 +++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000 @@ -1,4 +1,4 @@ - N/A \| Chars 27 - 68 [Declare~Reduction~comp~:=~nati] \| ms \|\| -ms \| N/A + N/A \| Chars 27 - 68 [Declare~Reduction~comp~:=~nati] \| ms \|\| -ms \| -% ------ ------ After \| Code \| Before \|\| Change \| % Change ``` where, because `Declare Reduction` takes 0.006s rather than 0s, the % change shows up as -100% rather than N/A.
\| \| \| \| \| \| \| \| \| * / / / / /	Fix #6404 - Print tactics called by ML tactics	Jason Gross	2018-04-02
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	[api] Move some types to their proper module.	Emilio Jesus Gallego Arias	2018-04-02
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We solve some modularity and type duplication problems by moving types to a better place. In particular: - We move tactics types from `Misctypes` to `Tactics` as this is their proper module an single user [with LTAC]. - We deprecate aliases in `Tacexpr` to such tactic types. cc: #6512
* \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[toplevel] Protect goal printing better wrt Break [fixes #7142]	Emilio Jesus Gallego Arias	2018-04-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When interrupting goal printing, we should continue the loop with the newly generated state, that should help avoiding synchronization problems as in #7142. Fixes #7142.