aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR#846: Fix OS X Travis by pinning OCaml version.Gravatar Maxime Dénès2017-06-30
|\
* \ Merge PR#843: closing bug #5618 introduce by PR 828Gravatar Maxime Dénès2017-06-30
|\ \
| | * Fix OS X Travis by pinning OCaml version.Gravatar Théo Zimmermann2017-06-30
| |/ |/|
| * closing bug #5618 introduce by PR 828Gravatar Julien Forest2017-06-29
| |
* | Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Gravatar Maxime Dénès2017-06-27
|\ \ | | | | | | | | | with make -j4
* \ \ Merge PR#826: Put plugin exports in the right compatibility fileGravatar Maxime Dénès2017-06-26
|\ \ \
* \ \ \ Merge PR#825: Ignore all PDF files.Gravatar Maxime Dénès2017-06-26
|\ \ \ \
* \ \ \ \ Merge PR#828: closing bug #4250Gravatar Maxime Dénès2017-06-26
|\ \ \ \ \ | | |_|_|/ | |/| | |
* | | | | Merge PR#824: Fix printersGravatar Maxime Dénès2017-06-23
|\ \ \ \ \
* \ \ \ \ \ Merge PR#821: [vernac] Remove stale bool parameter from ↵Gravatar Maxime Dénès2017-06-23
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | `VernacStartTheoremProof`
* \ \ \ \ \ \ Merge PR#820: [ide] Correct more merging errors.Gravatar Maxime Dénès2017-06-23
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#815: STM: par: report no error to UIs in non-solve modeGravatar Maxime Dénès2017-06-23
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#794: Cleanup of ltac cmxsGravatar Maxime Dénès2017-06-23
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#762: [vernac] Fix unneeded mutual references in ObligationsGravatar Maxime Dénès2017-06-23
|\ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | closing bug #4250Gravatar Julien Forest2017-06-23
| |_|_|_|_|_|/ / / / |/| | | | | | | | |
| | | | | | | | * | Add test-suite file for funind, extraction with compat 8.6Gravatar Jason Gross2017-06-22
| | | | | | | | | |
| | | | | | | | * | Put plugin exports in the right compatibility fileGravatar Jason Gross2017-06-22
| |_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607). PR #220 put the exports in the wrong compat files, presumably because it was originally targeted to version 8.6, and this wasn't updated when it was retargeted to version 8.7.
| | | | | | | * | Ignore all PDF files.Gravatar Théo Zimmermann2017-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Rules for ignoring *some* PDF files had been added one by one to `.gitignore` but some were still missing (for the corresponding latex files in `dev`). This rule is actually better since we are not tracking any PDF file.
* | | | | | | | | Merge PR#817: [stm] Fix route setting on VtQueryGravatar Maxime Dénès2017-06-22
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / |/| | | | | | | |
| | | | | | | * | Add missing definition and fix #use include;; as suggested by @amintimany.Gravatar Théo Zimmermann2017-06-22
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
| |_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
| | | | | * | [ide] Correct more merging errors.Gravatar Emilio Jesus Gallego Arias2017-06-21
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | This file doesn't want to leave us.
| | | | | * Should fix a false negative reported by deps-order.sh.Gravatar Hugo Herbelin2017-06-21
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
| * | | | [stm] Fix route setting on VtQueryGravatar Emilio Jesus Gallego Arias2017-06-20
|/ / / / | | | | | | | | | | | | | | | | | | | | This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter.
| | | * STM: par: report no error to UIs in non-solve modeGravatar Enrico Tassi2017-06-20
| | | | | | | | | | | | | | | | | | | | | | | | Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve")
| * | | [vernac] Remove forward hooks from Obligations.Gravatar Emilio Jesus Gallego Arias2017-06-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
| * | | [vernac] Remove unused hooks.Gravatar Emilio Jesus Gallego Arias2017-06-20
|/ / / | | | | | | | | | These hooks are not used (leftovers?) and IMHO they should not be.
* | | Merge PR#742: Fix `make TIMED=1` garbageGravatar Maxime Dénès2017-06-20
|\ \ \
* \ \ \ Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \ \ \
* \ \ \ \ Merge PR#793: Fixing restriction of existential variables regarding evar_storeGravatar Maxime Dénès2017-06-20
|\ \ \ \ \
* \ \ \ \ \ Merge PR#807: romega: fix a slowdownGravatar Maxime Dénès2017-06-20
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#803: Clean ssrGravatar Maxime Dénès2017-06-20
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#790: Direct link to Travis branch builds.Gravatar Maxime Dénès2017-06-20
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR#779: Each user overlay goes into its own file.Gravatar Maxime Dénès2017-06-20
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR#777: Improving documentation of tactic "move" (report #4561)Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR#760: Fixing base_include after loc is an option + a better test ↵Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | that #use"include" works
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#795: [ide] Better exn printing. [fixes BZ#5524]Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#613: Cumulativity for inductive typesGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | | | | Test case for bug 5578.Gravatar Maxime Dénès2017-06-19
| | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR#727: [tactics] Fix summary registration of global hint variable.Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | | | | | Fix typo in comment.Gravatar Maxime Dénès2017-06-19
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | Merge PR#784: API additions for coq-dpdgraphGravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR#755: "There are pending proofs" error message now lists the name of ↵Gravatar Maxime Dénès2017-06-19
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | the proofs.
| | | | | | | | | | | | | | * | | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
| | | | | * | | | | | | | | | | | [ide] Better exn printing. [fixes BZ#5524]Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | |_|_|_|_|_|_|_|/ / / | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies.
* | | | | | | | | | | | | | | | Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.Gravatar Maxime Dénès2017-06-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | * | | | romega: avoid potential slowdown when changing concl by reified versionGravatar Pierre Letouzey2017-06-16
| | | | | | | |_|_|_|_|_|/ / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP.
* | | | | | | | | | | | | | | | Merge PR#759: don't leak unqualified identifiers from the macroGravatar Maxime Dénès2017-06-16
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | * | | | | | | | | | | | Add coq-dpdgraph to gitlab CIGravatar Gaëtan Gilbert2017-06-16
| | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:37:50 +0000