aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-29closing bug #5618 introduce by PR 828Julien Forest
2017-06-27Merge PR#810: An attempt to fix a failure of test deps-checksum.sh fails ↵Maxime Dénès
with make -j4
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-26Merge PR#825: Ignore all PDF files.Maxime Dénès
2017-06-26Merge PR#828: closing bug #4250Maxime Dénès
2017-06-23Merge PR#824: Fix printersMaxime Dénès
2017-06-23Merge PR#821: [vernac] Remove stale bool parameter from ↵Maxime Dénès
`VernacStartTheoremProof`
2017-06-23Merge PR#820: [ide] Correct more merging errors.Maxime Dénès
2017-06-23Merge PR#815: STM: par: report no error to UIs in non-solve modeMaxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-23Merge PR#762: [vernac] Fix unneeded mutual references in ObligationsMaxime Dénès
2017-06-23closing bug #4250Julien Forest
2017-06-22Add test-suite file for funind, extraction with compat 8.6Jason Gross
2017-06-22Put plugin exports in the right compatibility fileJason Gross
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.
2017-06-22Ignore all PDF files.Théo Zimmermann
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.
2017-06-22Merge PR#817: [stm] Fix route setting on VtQueryMaxime Dénès
2017-06-22Add missing definition and fix #use include;; as suggested by @amintimany.Théo Zimmermann
2017-06-21[vernac] Remove stale bool parameter from `VernacStartTheoremProof`Emilio Jesus Gallego Arias
`VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
2017-06-21[ide] Correct more merging errors.Emilio Jesus Gallego Arias
This file doesn't want to leave us.
2017-06-21Should fix a false negative reported by deps-order.sh.Hugo Herbelin
The files deps-order.sh and deps-checksum.sh were concurrently rm-ing the files of the other. Courtesy of Guillaume M.
2017-06-20[stm] Fix route setting on VtQueryEmilio Jesus Gallego Arias
This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter.
2017-06-20STM: par: report no error to UIs in non-solve modeEnrico Tassi
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")
2017-06-20[vernac] Remove forward hooks from Obligations.Emilio Jesus Gallego Arias
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.
2017-06-20[vernac] Remove unused hooks.Emilio Jesus Gallego Arias
These hooks are not used (leftovers?) and IMHO they should not be.
2017-06-20Merge PR#742: Fix `make TIMED=1` garbageMaxime Dénès
2017-06-20Merge PR#774: [ide] Add route_id parameter to query call.Maxime Dénès
2017-06-20Merge PR#793: Fixing restriction of existential variables regarding evar_storeMaxime Dénès
2017-06-20Merge PR#807: romega: fix a slowdownMaxime Dénès
2017-06-20Merge PR#803: Clean ssrMaxime Dénès
2017-06-20Merge PR#790: Direct link to Travis branch builds.Maxime Dénès
2017-06-20Merge PR#779: Each user overlay goes into its own file.Maxime Dénès
2017-06-19Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalMaxime Dénès
2017-06-19Merge PR#777: Improving documentation of tactic "move" (report #4561)Maxime Dénès
2017-06-19Merge PR#760: Fixing base_include after loc is an option + a better test ↵Maxime Dénès
that #use"include" works
2017-06-19Merge PR#795: [ide] Better exn printing. [fixes BZ#5524]Maxime Dénès
2017-06-19Merge PR#613: Cumulativity for inductive typesMaxime Dénès
2017-06-19Test case for bug 5578.Maxime Dénès
2017-06-19Merge PR#727: [tactics] Fix summary registration of global hint variable.Maxime Dénès
2017-06-19Fix typo in comment.Maxime Dénès
2017-06-19Merge PR#784: API additions for coq-dpdgraphMaxime Dénès
2017-06-19Merge PR#755: "There are pending proofs" error message now lists the name of ↵Maxime Dénès
the proofs.
2017-06-18[ide] Add route_id parameter to query call.Emilio Jesus Gallego Arias
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 ####.
2017-06-18[ide] Better exn printing. [fixes BZ#5524]Emilio Jesus Gallego Arias
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.
2017-06-16Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.Maxime Dénès
2017-06-16romega: avoid potential slowdown when changing concl by reified versionPierre Letouzey
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.
2017-06-16Merge PR#759: don't leak unqualified identifiers from the macroMaxime Dénès
2017-06-16Add coq-dpdgraph to gitlab CIGaëtan Gilbert
2017-06-16"There are pending proofs" error message now lists the name of the proofs.Théo Zimmermann
This closes https://coq.inria.fr/bugs/show_bug.cgi?id=5275
2017-06-16Increase the time limit on 4366.v to make gitlab work better.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:34:50 +0000