aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-05Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Enrico Tassi
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-04-04Merge PR #7163: merge-pr.sh: cache github API callsMaxime Dénès
2018-04-04Merge PR #7158: [meta] Add `num` to the set of base libraries.Enrico Tassi
2018-04-04Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsPierre-Marie Pédrot
2018-04-04Merge PR #7147: [doc] Document better ocamlfind and flambda requirements.Théo Zimmermann
2018-04-04Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps ↵Enrico Tassi
with #7142]
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-04Merge PR #7104: Sphinx doc chapter 27Théo Zimmermann
2018-04-04Merge PR #7048: Sphinx doc chapter 25Théo Zimmermann
2018-04-04Merge PR #7049: Sphinx doc chapter 26Théo Zimmermann
2018-04-04Merge PR #7047: Sphinx doc chapter 24Théo Zimmermann
2018-04-04Merge PR #7041: Sphinx doc chapter 23Théo Zimmermann
2018-04-04Merge PR #7037: Sphinx doc chapter 18Théo Zimmermann
2018-04-03merge-pr.sh: cache github API callsGaëtan Gilbert
2018-04-03Merge PR #7154: Update coq_makefile timing testGaëtan Gilbert
2018-04-03[doc] Document better ocamlfind and flambda requirements.Emilio Jesus Gallego Arias
Closes #6782
2018-04-03[meta] Add `num` to the set of base libraries.Emilio Jesus Gallego Arias
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.
2018-04-02Update coq_makefile timing testJason Gross
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.
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-01Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of ↵Pierre-Marie Pédrot
tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-04-01Merge PR #7132: [doc] Add some more documentation to STM API.Enrico Tassi
2018-04-01Merge PR #6802: Remove deprecated commands Implicit Arguments and Arguments ↵Enrico Tassi
Scope
2018-04-01[toplevel] Protect goal printing better wrt Break [fixes #7142]Emilio Jesus Gallego Arias
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.
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
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.
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
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.
2018-03-31[doc] Add some more documentation to STM API.Emilio Jesus Gallego Arias
2018-03-31Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)Emilio Jesus Gallego Arias
2018-03-30Add CHANGES for removing Implicit Arguments and Arguments ScopeJasper Hugunin
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-31Merge PR #7121: Remove outdated patch from ci-sfEmilio Jesus Gallego Arias
2018-03-31Merge PR #6989: Enable whitespace checking for new Sphinx file extensions.Emilio Jesus Gallego Arias
2018-03-31Merge PR #7111: Fix #6631: Derive Plugin gives "Anomaly: more than one ↵Emilio Jesus Gallego Arias
statement".
2018-03-31Linter: verify overlay extensions.Gaëtan Gilbert
2018-03-31pre-commit: verify user overlay extensions (must be .sh).Gaëtan Gilbert
This has come up a couple times.
2018-03-31Merge PR #7130: gitlab: fix environment for build templateEmilio Jesus Gallego Arias
2018-03-30[Sphinx] Add chapter 27Maxime Dénès
Thanks to Calvin Beck for porting this chapter.
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Add chapter 25Maxime Dénès
Thanks to Laurent Théry for porting this chapter.
2018-03-30[Sphinx] Move chapter 25 to new infrastructureMaxime Dénès
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
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.
2018-03-30gitlab: fix environment for build templateGaëtan Gilbert
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.
2018-03-29Remove outdated patch from ci-sfJasper Hugunin
2018-03-29[Sphinx] Add chapter 26Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-03-29[Sphinx] Move chapter 26 to new infrastructureMaxime Dénès
2018-03-29Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Pierre-Marie Pédrot
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.
2018-03-29[Sphinx] Add chapter 24Maxime Dénès
Thanks to Matthieu Sozeau for porting this chapter.
2018-03-29[Sphinx] Move chapter 24 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 16:59:23 +0000