aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps ↵Gravatar Enrico Tassi2018-04-04
|\ | | | | | | with #7142]
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
* \ \ Merge PR #7104: Sphinx doc chapter 27Gravatar Théo Zimmermann2018-04-04
|\ \ \
* \ \ \ Merge PR #7048: Sphinx doc chapter 25Gravatar Théo Zimmermann2018-04-04
|\ \ \ \
* \ \ \ \ Merge PR #7049: Sphinx doc chapter 26Gravatar Théo Zimmermann2018-04-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7047: Sphinx doc chapter 24Gravatar Théo Zimmermann2018-04-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7041: Sphinx doc chapter 23Gravatar Théo Zimmermann2018-04-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7037: Sphinx doc chapter 18Gravatar Théo Zimmermann2018-04-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7154: Update coq_makefile timing testGravatar Gaëtan Gilbert2018-04-03
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | Update coq_makefile timing testGravatar Jason Gross2018-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.
* | | | | | | | | Merge PR #6844: Adding tclBINDFIRST/tclBINDLAST, generalizing type of ↵Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tclTHENFIRST/tclTHENLAST, informative version of shelve unifiable
* \ \ \ \ \ \ \ \ \ Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7132: [doc] Add some more documentation to STM API.Gravatar Enrico Tassi2018-04-01
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6802: Remove deprecated commands Implicit Arguments and Arguments ↵Gravatar Enrico Tassi2018-04-01
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Scope
| | | | | | | | | | | | * [toplevel] Protect goal printing better wrt Break [fixes #7142]Gravatar Emilio Jesus Gallego Arias2018-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] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-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.Gravatar Emilio Jesus Gallego Arias2018-03-31
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6950: pre-commit, linter: verify user overlay extensions (must be sh)Gravatar Emilio Jesus Gallego Arias2018-03-31
|\ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | Add CHANGES for removing Implicit Arguments and Arguments ScopeGravatar Jasper Hugunin2018-03-30
| | | | | | | | | | |
| | * | | | | | | | | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
| | | | | | | | | | |
| | * | | | | | | | | Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
| |/ / / / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #7121: Remove outdated patch from ci-sfGravatar Emilio Jesus Gallego Arias2018-03-31
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6989: Enable whitespace checking for new Sphinx file extensions.Gravatar Emilio Jesus Gallego Arias2018-03-31
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7111: Fix #6631: Derive Plugin gives "Anomaly: more than one ↵Gravatar Emilio Jesus Gallego Arias2018-03-31
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | statement".
| | | | * | | | | | | | | Linter: verify overlay extensions.Gravatar Gaëtan Gilbert2018-03-31
| | | | | | | | | | | | |
| | | | * | | | | | | | | pre-commit: verify user overlay extensions (must be .sh).Gravatar Gaëtan Gilbert2018-03-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This has come up a couple times.
* | | | | | | | | | | | | Merge PR #7130: gitlab: fix environment for build templateGravatar Emilio Jesus Gallego Arias2018-03-31
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | | | | * [Sphinx] Add chapter 27Gravatar Maxime Dénès2018-03-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Calvin Beck for porting this chapter.
| | | | | | | | | | | | * [Sphinx] Move chapter 27 to new infrastructureGravatar Maxime Dénès2018-03-30
| | | | | | | | | | | |/
| | | | | | | | | | | * [Sphinx] Add chapter 25Gravatar Maxime Dénès2018-03-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Laurent Théry for porting this chapter.
| | | | | | | | | | | * [Sphinx] Move chapter 25 to new infrastructureGravatar Maxime Dénès2018-03-30
| | | | | | | | | | |/
| * | | | | | | | | / gitlab: fix environment for build templateGravatar Gaëtan Gilbert2018-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-sfGravatar Jasper Hugunin2018-03-29
| |_|/ / / / / / / |/| | | | | | | |
| | | | | | | | * [Sphinx] Add chapter 26Gravatar Maxime Dénès2018-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Paul Steckler for porting this chapter.
| | | | | | | | * [Sphinx] Move chapter 26 to new infrastructureGravatar Maxime Dénès2018-03-29
| | | | | | | |/
| * | | | | | / Fix #6631: Derive Plugin gives "Anomaly: more than one statement".Gravatar Pierre-Marie Pédrot2018-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.
| | | | | | * [Sphinx] Add chapter 24Gravatar Maxime Dénès2018-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Thanks to Matthieu Sozeau for porting this chapter.
| | | | | | * [Sphinx] Move chapter 24 to new infrastructureGravatar Maxime Dénès2018-03-29
| | | | | |/
| | | | | * [Sphinx] Add chapter 23Gravatar Maxime Dénès2018-03-29
| | | | | | | | | | | | | | | | | | | | | | | | Thanks to Pierre Letouzey for porting this chapter.
| | | | | * [Sphinx] Move chapter 23 to new infrastructureGravatar Maxime Dénès2018-03-29
| | | | |/
| | | | * [Sphinx] Remove duplicate entry for command `Coercion`Gravatar Maxime Dénès2018-03-29
| | | | |
| | | | * [Sphinx] Add chapter 18Gravatar Maxime Dénès2018-03-29
| | | | | | | | | | | | | | | | | | | | Thanks to Pierre Letouzey for porting this chapter.
| | | | * [Sphinx] Move chapter 18 to new infrastructureGravatar Maxime Dénès2018-03-29
| |_|_|/ |/| | |
* | | | Merge PR #7057: Sphinx Chapter 20: Type ClassesGravatar Maxime Dénès2018-03-29
|\ \ \ \
* \ \ \ \ Merge PR #7072: Update codeownersGravatar Maxime Dénès2018-03-29
|\ \ \ \ \
| * | | | | Remove dev/doc/changes.md from files with a code owner.Gravatar Théo Zimmermann2018-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).Gravatar Hugo Herbelin2018-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.Gravatar Hugo Herbelin2018-03-28
| | | | | |
| | | | * | Adding Array.fold_left4.Gravatar Hugo Herbelin2018-03-28
| | | | | |
| | | | * | Detyping: Adding a variant of share_names for patterns.Gravatar Hugo Herbelin2018-03-28
| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:18:00 +0000