| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-04 | Merge remote-tracking branch 'github/pr/378' into v8.6 | Maxime Dénès | |
| Was PR#378: Univs: fix bug #5188 | |||
| 2016-12-02 | Fix test-suite after change in "context" printing. | Maxime Dénès | |
| 2016-12-02 | Merge remote-tracking branch 'github/pr/377' into v8.6 | Maxime Dénès | |
| Was PR#377: Univs: fix bug #5180 | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/372' into v8.6 | Maxime Dénès | |
| Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/368' into v8.6 | Maxime Dénès | |
| Was PR#368: Add example in dev/doc/changes involving Tacmach.project | |||
| 2016-12-02 | Merge branch 'pr/367' into v8.6 | Maxime Dénès | |
| Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility | |||
| 2016-12-02 | Fixing lexing of strings in comments for beautifier. | Hugo Herbelin | |
| Was a bug introduced in 0ad6edc1. | |||
| 2016-12-02 | Fixing printing of "ltac:" in tactics after surrounding parentheses | Hugo Herbelin | |
| became mandatory. | |||
| 2016-12-02 | Comment on universe handling in Parameters | Matthieu Sozeau | |
| 2016-12-02 | Univs: fix bug #5188 | Matthieu Sozeau | |
| Parameter was implemented the wrong way trying to separate the universes of the telescope. | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/381' into v8.6 | Maxime Dénès | |
| Was PR#381: V8.6+fix typeclasses eauto shelving | |||
| 2016-12-02 | Fix #5242 - Dubious unsilenceable warning on invalid identifier | Maxime Dénès | |
| We make this warning configurable and disabled by default. | |||
| 2016-12-02 | Fixing printing of "Set Warnings Append". | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing "Context". | Hugo Herbelin | |
| 2016-12-02 | Fixing printers for pr_auto_using and pr_firstorder_using. | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing several list of implicit arguments. | Hugo Herbelin | |
| 2016-12-02 | Fixing printing of "only parsing" in abbreviations. | Hugo Herbelin | |
| 2016-12-02 | Protect printing of ltac's "context [...]" from possible collision | Hugo Herbelin | |
| with user-level notations by inserting spaces. | |||
| 2016-12-02 | More on fixing #5098 (preserving printing of "in hyp"). | Hugo Herbelin | |
| 2016-12-02 | Merge remote-tracking branch 'github/pr/380' into v8.6 | Maxime Dénès | |
| Was PR#380: Fix bug #5232: proper globalization of hints paths | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/369' into v8.6 | Maxime Dénès | |
| Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/371' into v8.6 | Maxime Dénès | |
| Was PR#371: Update dev/doc/changes with things about mem_named_context | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/364' into v8.6 | Maxime Dénès | |
| Was PR#364: Add missing label. Fixes broken ref. | |||
| 2016-12-02 | Merge remote-tracking branch 'github/pr/382' into v8.6 | Maxime Dénès | |
| Was PR#382: [merlin] Adjust merlin for ide. | |||
| 2016-11-30 | [merlin] Adjust merlin for ide. | Emilio Jesus Gallego Arias | |
| 2016-11-30 | Fix shelving order in typeclasses eauto. | Théo Zimmermann | |
| Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved. | |||
| 2016-11-30 | Fix typeclasses eauto shelving. | Théo Zimmermann | |
| A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl. | |||
| 2016-11-30 | Fix bug #5232: proper globalization of hints paths | Matthieu Sozeau | |
| 2016-11-30 | Univs: fix bug #5180 | Matthieu Sozeau | |
| In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel. | |||
| 2016-11-30 | Fix #5183 - Two CoqIDE crash errors | Maxime Dénès | |
| When opening a file without extension, an uncaught exception was occurring. Note that this fix is not complete, since the "Compile Buffer" command still fails. This is because of a limitation of coqc which appends the ".v" extension to its argument even if it already existed (and even if it doesn't exist with the extension!). | |||
| 2016-11-30 | Update copyright on documentation cover. | Maxime Dénès | |
| 2016-11-30 | Fix #5174: Underinformative syntax error messages in the new arguments syntax | Maxime Dénès | |
| We introduce a bit of compatibility parsing code to print deprecation warnings. | |||
| 2016-11-29 | STM: cur_id must be invalid if an error occurs (fix #5191) | Enrico Tassi | |
| Line erroneously removed in 17f3346c | |||
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | |||
| 2016-11-24 | Lazily load constants in micromega (bug #5134). | Guillaume Melquiond | |
| 2016-11-24 | Fix some documentation typos. | Guillaume Melquiond | |
| 2016-11-24 | Fix incorrect long multiplication in the VM. | Guillaume Melquiond | |
| If the result had its 30th bit set, then all the high part of the result on a 64-bit architecture would end up being set, thus breaking subsequent computations. This patch also fixes the incorrectly parenthesized definition of uint32_of_value, which by luck was never misused. | |||
| 2016-11-22 | Properly parenthesize "ltac:" arguments (bug #5169). | Guillaume Melquiond | |
| 2016-11-21 | (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes | Jason Gross | |
| 2016-11-21 | (v8.6) Update dev/doc/changes with things about mem_named_context | Jason Gross | |
| 2016-11-21 | (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes | Jason Gross | |
| 2016-11-21 | (v8.6) Add example in dev/doc/changes involving Tacmach.project | Jason Gross | |
| 2016-11-21 | Remove spurious spaces in merlin file generated by coq_makefile (bug #5213). | Guillaume Melquiond | |
| 2016-11-21 | Stop parsing -compat-notations options, which are no longer supported (bug ↵ | Guillaume Melquiond | |
| #3339). | |||
| 2016-11-18 | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" | Maxime Dénès | |
| This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration. | |||
| 2016-11-18 | Revert "fake_ide: use the now available Status XML message" | Maxime Dénès | |
| This reverts commit 81c9fa0de99400b51c029cdbd1519b4f724e320a. | |||
| 2016-11-17 | Add missing label. Fixes broken ref. | Théo Zimmermann | |
| 2016-11-17 | fake_ide: use the now available Status XML message | Enrico Tassi | |
| 2016-11-17 | Merge remote-tracking branch 'github/pr/360' into v8.6 | Maxime Dénès | |
| Was PR#360: [stm] Remove STM-related vernaculars | |||
| 2016-11-17 | Merge commit '633ed9c' into v8.6 | Maxime Dénès | |
| Was PR#192: Add test suite files for 4700-4785 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |