aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | | | | | | * | | | | | | | [meta] Add `num` to the set of base libraries.Gravatar Emilio Jesus Gallego Arias2018-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 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.
| | | | | | | | | * / / / / / / / Fix #6404 - Print tactics called by ML tacticsGravatar Jason Gross2018-04-02
| |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-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 ↵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] More cleanup of "classification is not an interpreter"Gravatar Emilio Jesus Gallego Arias2018-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.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
| | | | | | | | | | |/ / / / / /
| | | | | | | | | | | * / / / / Fix #6257: anomaly with Printing Projections and Context.Gravatar Gaëtan Gilbert2018-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 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
| | | | | | | | | |
| | | | * | | | | | Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).Gravatar Hugo Herbelin2018-03-28
| | | | | | | | | |
| | | | * | | | | | Patternops: renaming an internal function to more closely match its effect.Gravatar Hugo Herbelin2018-03-28
| | | | | | | | | |
| | | | * | | | | | Glob_ops: cosmetic renaming to reflect the type of objects.Gravatar Hugo Herbelin2018-03-28
| | | | | | | | | |
* | | | | | | | | | Merge PR #7090: stm: don't propagate side effects when editing a proofGravatar Emilio Jesus Gallego Arias2018-03-28
|\ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 22:40:50 +0000