| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-13 | Selection of the current word in CoqIDE looks at all buffers. | Pierre-Marie Pédrot | |
| 2015-02-13 | Trying to fix bug #3930. | Pierre-Marie Pédrot | |
| Instead of setting the last modified part of the text to be the insert point, we register all modifications to the buffer between to user actions and take the last modified point to be the least offset of all those modifications. | |||
| 2015-02-12 | Fixed test-suite file, that should always work. | Matthieu Sozeau | |
| 2015-02-12 | Add test-suite files for closed bugs. | Matthieu Sozeau | |
| 2015-02-12 | Tentative fix for CoqIDE randomly dropping deletions. | Pierre-Marie Pédrot | |
| We make the deletion callback not to regenerate a task id, as the insertion callback does. I can't find a particular reason for this dissymetry, and it was indeed causing trouble. | |||
| 2015-02-12 | COMPATIBILITY: add note about the change of behavior of Instance foo := | Matthieu Sozeau | |
| {| |}. Add test-suite files for closed bugs. | |||
| 2015-02-12 | Univs: fix bug #4031: wrong folding of sigma in change. | Matthieu Sozeau | |
| 2015-02-12 | Univs: fix bug #3978: carry around the universe context used to | Matthieu Sozeau | |
| typecheck with definitions and thread it accordingly when typechecking module expressions. | |||
| 2015-02-12 | Fix bug #2775: Correct handling of universes in leminv. | Matthieu Sozeau | |
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi | |
| 2015-02-12 | Fixing bug #3261. | Pierre-Marie Pédrot | |
| 2015-02-12 | Focussing on message view in CoqIDE when a message is pushed. | Pierre-Marie Pédrot | |
| Also fixes bug #4030. | |||
| 2015-02-12 | Revert "Using same code for browsing physical directories in coqtop and coqdep." | Hugo Herbelin | |
| (Sorry, was not intended to be pushed) This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c. | |||
| 2015-02-12 | Revert "Capital letter in plugins." (Sorry, was not intended to be pushed) | Hugo Herbelin | |
| This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767. | |||
| 2015-02-12 | Capital letter in plugins. | Hugo Herbelin | |
| 2015-02-12 | Using same code for browsing physical directories in coqtop and coqdep. | Hugo Herbelin | |
| In particular: - abstracting the code using calls to Unix opendir, stat, and closedir, - uniformly using warnings when a directory does not exist (coqtop was ignoring silently and coqdep was exiting via handle_unix_error). | |||
| 2015-02-12 | Fixing #3982 (conflict with max notation for universes). | Hugo Herbelin | |
| 2015-02-12 | Fixing #3997 (occur-check in the presence of primitive projections, patch | Hugo Herbelin | |
| from Matthieu). | |||
| 2015-02-12 | Fixing bug #4023. | Pierre-Marie Pédrot | |
| 2015-02-12 | Fixing compilation for 3.12. | Pierre-Marie Pédrot | |
| 2015-02-12 | Tentative fix for bug #4027. | Pierre-Marie Pédrot | |
| 2015-02-12 | Make clearer that "Remove Printing Let" does not influence destructuring let. | Guillaume Melquiond | |
| 2015-02-11 | Adding test for bug #3786. | Pierre-Marie Pédrot | |
| 2015-02-11 | Missing space in error message | Matěj Grabovský | |
| 2015-02-11 | Win: use .exe extension for the ocaml compiler (Close 3572) | Enrico Tassi | |
| 2015-02-11 | STM: is Flags.async_proofs_full then always delegate | Enrico Tassi | |
| Probably a regression introduced in some code refactoring. Affects only PIDE based code. | |||
| 2015-02-11 | Fixing bug #4019, and checker blow-up at once. | Pierre-Marie Pédrot | |
| 2015-02-11 | Clarifying the implementation of universe hashconsing. | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding a statistic function on hashconsing tables. | Pierre-Marie Pédrot | |
| 2015-02-11 | Tactic Notation: use stable unique key for notations (Close: 3970) | Enrico Tassi | |
| This is a fixup of commit 2e09a22b that used uniquely generated kernel names but forgot to substitute them. | |||
| 2015-02-11 | Adding a test-suite for tactic notation naming. | Pierre-Marie Pédrot | |
| 2015-02-11 | Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307) | Guillaume Melquiond | |
| 2015-02-11 | Adding test for bug #3900. | Pierre-Marie Pédrot | |
| 2015-02-11 | Fixing bug #3900. | Pierre-Marie Pédrot | |
| 2015-02-11 | Reinstauring backtrace display in CoqIDE. | Pierre-Marie Pédrot | |
| 2015-02-10 | Avoid html markup inside tex files and fix url. | Guillaume Melquiond | |
| 2015-02-10 | Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195) | Guillaume Melquiond | |
| 2015-02-10 | Fixing #4001 (missing type constraints when building return clause of match). | Hugo Herbelin | |
| 2015-02-10 | Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in ↵ | Hugo Herbelin | |
| coqtop mode. | |||
| 2015-02-10 | Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ↵ | Hugo Herbelin | |
| declarations). | |||
| 2015-02-10 | Fixing #4018 (uncaught exception on non-equality in intros [=]). | Hugo Herbelin | |
| 2015-02-10 | A few refinements in whodidwhat 8.4. | Hugo Herbelin | |
| 2015-02-10 | Fix typeops ignoring results of check functions with let _, and one | Matthieu Sozeau | |
| safety hole in judge_of_constant_knowing parameters which was not checking the result of the check correctly (the rest of the calls in that file and all of the checker have been checked). | |||
| 2015-02-10 | Add section numbering to the refman PDF. (Fix for bug #2365) | Guillaume Melquiond | |
| 2015-02-10 | Prevent Latex from messing with backticks. (Fix for bug #3871) | Guillaume Melquiond | |
| 2015-02-10 | Fix documentation of generalize. (Fix for bug #4015) | Guillaume Melquiond | |
| 2015-02-10 | Fix some documentation typo. | Guillaume Melquiond | |
| 2015-02-10 | Granting wish #4008. | Pierre-Marie Pédrot | |
| 2015-02-10 | Test for bug #4012. | Pierre-Marie Pédrot | |
| 2015-02-10 | More expressive API for tclWITHHOLES. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |