aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Test for #2946 (trunk bug with let's in unification).Gravatar Hugo Herbelin2015-02-16
* Fixing test for bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Test for bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Fixing bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Fixing bug #4037.Gravatar Pierre-Marie Pédrot2015-02-15
* Changing default for CoqIDE project to append arguments.Gravatar Pierre-Marie Pédrot2015-02-15
* CoqIDE now remembers the path of the last opened project.Gravatar Pierre-Marie Pédrot2015-02-15
* Selecting whole words on double-click in CoqIDE.Gravatar Pierre-Marie Pédrot2015-02-15
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
* Reset "section name" works again (Close #3933)Gravatar Enrico Tassi2015-02-15
* Fix test-suite file. Check that definitions do work when sharing isGravatar Matthieu Sozeau2015-02-15
* Fix 'don't expose cases' in cbnGravatar Pierre Boutillier2015-02-15
* Note about "Undo. Undo." in CHANGESGravatar Enrico Tassi2015-02-15
* Test for bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* Fixing bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* Test for bug #3916.Gravatar Pierre-Marie Pédrot2015-02-15
* Fixing bug #3916.Gravatar Pierre-Marie Pédrot2015-02-15
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2015-02-15
* Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749)Gravatar Guillaume Melquiond2015-02-15
* Win: update READMEGravatar Enrico Tassi2015-02-14
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-14
* CoqIDE: restore old default colorsGravatar Enrico Tassi2015-02-14
* typoGravatar Enrico Tassi2015-02-14
* Attempt to be more colorblind friendly in CoqIDE (Close #4024)Gravatar Enrico Tassi2015-02-14
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Makefile: in byte we can always dynlinkGravatar Enrico Tassi2015-02-14
* Test for bug #4016.Gravatar Pierre-Marie Pédrot2015-02-14
* Fixing bug #4016.Gravatar Pierre-Marie Pédrot2015-02-14
* dependent destruction: Fix (part of) bug #3961, by fixing dependent *Gravatar Matthieu Sozeau2015-02-14
* coqc accepts -top option. Fixes bug #4043.Gravatar Pierre-Marie Pédrot2015-02-14
* Univs: fix bug #3755. We were missing refreshements of universes inGravatar Matthieu Sozeau2015-02-14
* Univs: When computing the level of an inductive including indices, letsGravatar Matthieu Sozeau2015-02-14
* Document the issue with trivial inductive types. (Workaround for bug #3984)Gravatar Guillaume Melquiond2015-02-13
* Fixup version & copyright for MacOS bundleGravatar Pierre Boutillier2015-02-13
* Hardcode how coqide have to look for coqtop in MacOS bundleGravatar Pierre Boutillier2015-02-13
* Better error message for nested module application.Gravatar Maxime Dénès2015-02-13
* Fix test-suite file to finishGravatar Matthieu Sozeau2015-02-13
* Selection of the current word in CoqIDE looks at all buffers.Gravatar Pierre-Marie Pédrot2015-02-13
* Trying to fix bug #3930.Gravatar Pierre-Marie Pédrot2015-02-13
* 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