| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2015-02-10 | Making undo/redo atomic in CoqIDE. | Pierre-Marie Pédrot | |
| 2015-02-10 | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot | |
| This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics. | |||
| 2015-02-09 | Fix bug #4014. | Pierre-Marie Pédrot | |
| 2015-02-07 | STM: tolerate simple side effects in async proofs (Close: 4006) | Enrico Tassi | |
| 2015-02-07 | Fixing bug #4009. | Pierre-Marie Pédrot | |
| We only allow color output under Unix OSes. | |||
| 2015-02-06 | More efficient Richpp. | Pierre-Marie Pédrot | |
| We build the rich XML at once without generating the printed string. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |