index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2015-02-20
A fix for #3993 (not fully applied term to destruct when eqn is given).
Hugo Herbelin
2015-02-19
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Pierre-Marie Pédrot
2015-02-19
Record type for VERNAC EXTEND rules and a bit of documentation.
Pierre-Marie Pédrot
2015-02-19
When looking for restrictions in ?n=?p problems, keep the type of let-bindings.
Hugo Herbelin
2015-02-18
Fix bug #3938
Matthieu Sozeau
2015-02-18
Fix bug #4046.
Matthieu Sozeau
2015-02-17
Deprecated options issue a warning.
Pierre-Marie Pédrot
2015-02-17
Remove Whelp commands.
Maxime Dénès
2015-02-17
Separate index for vernacular options.
Maxime Dénès
2015-02-17
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-16
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-15
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-14
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
[next]