coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| * \| \| \| \| \| \| \|	[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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	ssr: check cleared hyps do exist (fix #7050)	Enrico Tassi	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.
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[stm] More cleanup of "classification is not an interpreter"	Emilio Jesus Gallego Arias	2018-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \|/ / / / / / / \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove meta-information from the query classification and we don't process `Stm.query` as a transaction anymore, as the right API is available to it to execute the command directly. This simplifies pure commands and removes some impossible cases. Depends on #7138.
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias	2018-04-01
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This command is legacy, equivalent to `EditAt` and only used by Emacs. We move it to the toplevel so we can kill some legacy code and in particular the `part_of_script` hack.
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Add chapter 27	Maxime Dénès	2018-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Calvin Beck for porting this chapter.
\| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Move chapter 27 to new infrastructure	Maxime Dénès	2018-03-30
\| \| \| \| \| \| \| \| \| \| \| \|/ / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Add chapter 25	Maxime Dénès	2018-03-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Laurent Théry for porting this chapter.
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	[Sphinx] Move chapter 25 to new infrastructure	Maxime Dénès	2018-03-30
\| \| \| \| \| \| \| \| \| \| \|/ / / / / / / /
\| \| \| \| \| \| \| \| \| \| \| * / / / / / /	Fix #6257: anomaly with Printing Projections and Context.	Gaëtan Gilbert	2018-03-30
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Constrextern.explicitize expected that if implicits were declared they would be declared at least up to the principal argument of the projection, but Context/discharge of implicits does not preserve this. Note the anomaly only happens with primitive projections DISABLED in recent Coqs (>=8.8). Implicit argument experts may consider whether ensuring enough implicits are declared would be better.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fixes #7110 ("as" untested while looking for notation for nested patterns).	Hugo Herbelin	2018-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[Sphinx] Add chapter 26	Maxime Dénès	2018-03-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Thanks to Paul Steckler for porting this chapter.
\| \| \| \| \| \| \| \| * \| \| \| \| \| \|	[Sphinx] Move chapter 26 to new infrastructure	Maxime Dénès	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.