| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-02-15 | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond | |
| 2015-02-14 | Win: update README | Enrico Tassi | |
| 2015-02-14 | Fixing OCaml 3.12 compilation. | Pierre-Marie Pédrot | |
| 2015-02-14 | CoqIDE: restore old default colors | Enrico Tassi | |
| 2015-02-14 | typo | Enrico Tassi | |
| 2015-02-14 | Attempt to be more colorblind friendly in CoqIDE (Close #4024) | Enrico Tassi | |
| 2015-02-14 | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | |
| Of course such proofs cannot be processed asynchronously | |||
| 2015-02-14 | Makefile: in byte we can always dynlink | Enrico Tassi | |
| 2015-02-14 | Test for bug #4016. | Pierre-Marie Pédrot | |
| 2015-02-14 | Fixing bug #4016. | Pierre-Marie Pédrot | |
| When setoid rewriting in a hypothesis, we push the newly introduced declaration after the last declaration it depends on. | |||
| 2015-02-14 | dependent destruction: Fix (part of) bug #3961, by fixing dependent * | Matthieu Sozeau | |
| generalizing * which was broken since 8.4. | |||
| 2015-02-14 | coqc accepts -top option. Fixes bug #4043. | Pierre-Marie Pédrot | |
| 2015-02-14 | Univs: fix bug #3755. We were missing refreshements of universes in | Matthieu Sozeau | |
| unifications ?X ~= ?Y foo not catched by solve_evar_evar. | |||
| 2015-02-14 | Univs: When computing the level of an inductive including indices, lets | Matthieu Sozeau | |
| do not contribute. Fixes bug #3808. | |||
| 2015-02-13 | Document the issue with trivial inductive types. (Workaround for bug #3984) | Guillaume Melquiond | |
| 2015-02-13 | Fixup version & copyright for MacOS bundle | Pierre Boutillier | |
| 2015-02-13 | Hardcode how coqide have to look for coqtop in MacOS bundle | Pierre Boutillier | |
| Sorry, that is ugly. Please revert if you see a better way to do it. | |||
| 2015-02-13 | Better error message for nested module application. | Maxime Dénès | |
| Fixes #3809. | |||
| 2015-02-13 | Fix test-suite file to finish | Matthieu Sozeau | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |