index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
Remove documentation of non-existing Show Implicits command.
Maxime Dénès
2015-02-17
*
Remove non-existing Tactic Definition command from index.
Maxime Dénès
2015-02-17
*
Fix sentence that was cut in doc of Local Set.
Maxime Dénès
2015-02-17
*
Fixing bug #4053.
Pierre-Marie Pédrot
2015-02-17
*
Fixing bug #4023 again.
Pierre-Marie Pédrot
2015-02-17
*
Tentative fix for bug #2855.
Pierre-Marie Pédrot
2015-02-17
*
CoqIDE: read-only Qed sentence reflected in colors (Close: 4051)
Enrico Tassi
2015-02-17
*
Remove some dead code and add test-suite file.
Matthieu Sozeau
2015-02-16
*
Add test-suite file for #3960.
Matthieu Sozeau
2015-02-16
*
Better comment for [type_of_global_unsafe].
Matthieu Sozeau
2015-02-16
*
Comment on the unsafe_ functions in Global.
Matthieu Sozeau
2015-02-16
*
Test for bug #3922.
Pierre-Marie Pédrot
2015-02-16
*
STM: when async_proofs_full is set process only tasks in the perspective
Enrico Tassi
2015-02-16
*
*Queue: API to wake up all threads
Enrico Tassi
2015-02-16
*
Fix bug #3960: potential evar instance categorized as an unresolvable
Matthieu Sozeau
2015-02-16
*
Documenting "induction t in ctx" when ctx contains an hyp not mentioning t.
Hugo Herbelin
2015-02-16
*
Fixing bug #4035 (support for dependent destruction within ltac code).
Hugo Herbelin
2015-02-16
*
Test for #2946 (trunk bug with let's in unification).
Hugo Herbelin
2015-02-16
*
Fixing test for bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Test for bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Fixing bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Fixing bug #4037.
Pierre-Marie Pédrot
2015-02-15
*
Changing default for CoqIDE project to append arguments.
Pierre-Marie Pédrot
2015-02-15
*
CoqIDE now remembers the path of the last opened project.
Pierre-Marie Pédrot
2015-02-15
*
Selecting whole words on double-click in CoqIDE.
Pierre-Marie Pédrot
2015-02-15
*
Undo: back to 8.4 semantics (Close #3514)
Enrico Tassi
2015-02-15
*
Reset "section name" works again (Close #3933)
Enrico Tassi
2015-02-15
*
Fix test-suite file. Check that definitions do work when sharing is
Matthieu Sozeau
2015-02-15
*
Fix 'don't expose cases' in cbn
Pierre Boutillier
2015-02-15
*
Note about "Undo. Undo." in CHANGES
Enrico Tassi
2015-02-15
*
Test for bug #3490.
Pierre-Marie Pédrot
2015-02-15
*
Fixing bug #3490.
Pierre-Marie Pédrot
2015-02-15
*
Test for bug #3916.
Pierre-Marie Pédrot
2015-02-15
*
Fixing bug #3916.
Pierre-Marie Pédrot
2015-02-15
*
Fixing test-suite.
Pierre-Marie Pédrot
2015-02-15
*
Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749)
Guillaume Melquiond
2015-02-15
*
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
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
2015-02-14
*
dependent destruction: Fix (part of) bug #3961, by fixing dependent *
Matthieu Sozeau
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
2015-02-14
*
Univs: When computing the level of an inductive including indices, lets
Matthieu Sozeau
2015-02-14
*
Document the issue with trivial inductive types. (Workaround for bug #3984)
Guillaume Melquiond
2015-02-13
[prev]
[next]