aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* CoqIDE: read-only Qed sentence reflected in colors (Close: 4051)Gravatar Enrico Tassi2015-02-17
* Remove some dead code and add test-suite file.Gravatar Matthieu Sozeau2015-02-16
* Add test-suite file for #3960.Gravatar Matthieu Sozeau2015-02-16
* Better comment for [type_of_global_unsafe].Gravatar Matthieu Sozeau2015-02-16
* Comment on the unsafe_ functions in Global.Gravatar Matthieu Sozeau2015-02-16
* Test for bug #3922.Gravatar Pierre-Marie Pédrot2015-02-16
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
* *Queue: API to wake up all threadsGravatar Enrico Tassi2015-02-16
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
* Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.Gravatar Hugo Herbelin2015-02-16
* Fixing bug #4035 (support for dependent destruction within ltac code).Gravatar Hugo Herbelin2015-02-16
* 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