aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Fixed test-suite file, that should always work.Gravatar Matthieu Sozeau2015-02-12
* Add test-suite files for closed bugs.Gravatar Matthieu Sozeau2015-02-12
* Tentative fix for CoqIDE randomly dropping deletions.Gravatar Pierre-Marie Pédrot2015-02-12
* COMPATIBILITY: add note about the change of behavior of Instance foo :=Gravatar Matthieu Sozeau2015-02-12
* Univs: fix bug #4031: wrong folding of sigma in change.Gravatar Matthieu Sozeau2015-02-12
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Fix bug #2775: Correct handling of universes in leminv.Gravatar Matthieu Sozeau2015-02-12
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Fixing bug #3261.Gravatar Pierre-Marie Pédrot2015-02-12
* Focussing on message view in CoqIDE when a message is pushed.Gravatar Pierre-Marie Pédrot2015-02-12
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* Fixing #3982 (conflict with max notation for universes).Gravatar Hugo Herbelin2015-02-12
* Fixing #3997 (occur-check in the presence of primitive projections, patchGravatar Hugo Herbelin2015-02-12
* Fixing bug #4023.Gravatar Pierre-Marie Pédrot2015-02-12
* Fixing compilation for 3.12.Gravatar Pierre-Marie Pédrot2015-02-12
* Tentative fix for bug #4027.Gravatar Pierre-Marie Pédrot2015-02-12
* Make clearer that "Remove Printing Let" does not influence destructuring let.Gravatar Guillaume Melquiond2015-02-12
* Adding test for bug #3786.Gravatar Pierre-Marie Pédrot2015-02-11
* Missing space in error messageGravatar Matěj Grabovský2015-02-11
* Win: use .exe extension for the ocaml compiler (Close 3572)Gravatar Enrico Tassi2015-02-11
* STM: is Flags.async_proofs_full then always delegateGravatar Enrico Tassi2015-02-11
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
* Adding a statistic function on hashconsing tables.Gravatar Pierre-Marie Pédrot2015-02-11
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
* Adding a test-suite for tactic notation naming.Gravatar Pierre-Marie Pédrot2015-02-11
* Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Gravatar Guillaume Melquiond2015-02-11
* Adding test for bug #3900.Gravatar Pierre-Marie Pédrot2015-02-11
* Fixing bug #3900.Gravatar Pierre-Marie Pédrot2015-02-11
* Reinstauring backtrace display in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-11
* Avoid html markup inside tex files and fix url.Gravatar Guillaume Melquiond2015-02-10
* Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)Gravatar Guillaume Melquiond2015-02-10
* Fixing #4001 (missing type constraints when building return clause of match).Gravatar Hugo Herbelin2015-02-10
* Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Gravatar Hugo Herbelin2015-02-10
* Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Gravatar Hugo Herbelin2015-02-10
* Fixing #4018 (uncaught exception on non-equality in intros [=]).Gravatar Hugo Herbelin2015-02-10
* A few refinements in whodidwhat 8.4.Gravatar Hugo Herbelin2015-02-10
* Fix typeops ignoring results of check functions with let _, and oneGravatar Matthieu Sozeau2015-02-10
* Add section numbering to the refman PDF. (Fix for bug #2365)Gravatar Guillaume Melquiond2015-02-10
* Prevent Latex from messing with backticks. (Fix for bug #3871)Gravatar Guillaume Melquiond2015-02-10
* Fix documentation of generalize. (Fix for bug #4015)Gravatar Guillaume Melquiond2015-02-10
* Fix some documentation typo.Gravatar Guillaume Melquiond2015-02-10
* Granting wish #4008.Gravatar Pierre-Marie Pédrot2015-02-10
* Test for bug #4012.Gravatar Pierre-Marie Pédrot2015-02-10
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Making undo/redo atomic in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 07:53:36 +0000