aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-30Fix more potential quoting issues: COQBIN , COQLIBJason Gross
2017-06-30Also quote $(COQLIB)/grammarJason Gross
In case COQLIB has backslashes, as it does on Windows, or spaces
2017-06-30Create a variable for CAMLDOC in CoqMakefile.inJason Gross
2017-06-30Quote $(OCAMLFIND) in CoqMakefile.in for WindowsJason Gross
This, I hope, will fix [bug #5620](https://coq.inria.fr/bugs/show_bug.cgi?id=5620)
2017-06-30Merge PR#846: Fix OS X Travis by pinning OCaml version.Maxime Dénès
2017-06-30Merge PR#843: closing bug #5618 introduce by PR 828Maxime Dénès
2017-06-30Fix OS X Travis by pinning OCaml version.Théo Zimmermann
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 03:31:34 +0000