aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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 #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-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-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] 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-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
2018-03-29[Sphinx] Add chapter 23Maxime Dénès
Thanks to Pierre Letouzey for porting this chapter.
2018-03-29[Sphinx] Move chapter 23 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Remove duplicate entry for command `Coercion`Maxime Dénès
2018-03-29[Sphinx] Add chapter 18Maxime Dénès
Thanks to Pierre Letouzey for porting this chapter.
2018-03-29[Sphinx] Move chapter 18 to new infrastructureMaxime Dénès
2018-03-29Merge PR #7057: Sphinx Chapter 20: Type ClassesMaxime Dénès
2018-03-29Merge PR #7072: Update codeownersMaxime Dénès
2018-03-29Remove dev/doc/changes.md from files with a code owner.Théo Zimmermann
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.
2018-03-28Supporting fix/cofix in Ltac pattern-matching (wish #7092).Hugo Herbelin
This is done by not failing for fix/cofix while translating from glob_constr to constr_pattern.
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 23:15:30 +0000