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
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Fixing computation of implicit arguments by position in fixpoints (#4217).
Hugo Herbelin
2015-05-01
*
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-05-01
*
Improve syntax highlighting.
Guillaume Melquiond
2015-04-27
*
Compile the VM code with some optimizations (+130% speedup).
Guillaume Melquiond
2015-04-27
*
Fix some ill-typed debugging code in the VM.
Guillaume Melquiond
2015-04-27
*
Open the file chooser even if there is no current session. (Fix bug #4206)
Guillaume Melquiond
2015-04-26
*
Cleaning some uses of exceptions in tactics.
Pierre-Marie Pédrot
2015-04-25
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
Removing dead code in Pp.
Pierre-Marie Pédrot
2015-04-23
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Pp: obsolete comment.
Arnaud Spiwack
2015-04-22
*
Declarative mode: remaining goals are "given up" when closing blocks.
Arnaud Spiwack
2015-04-22
*
Fixing non exhaustive pattern-matching.
Hugo Herbelin
2015-04-22
*
Test for #4198 (appcontext in return clause of match).
Hugo Herbelin
2015-04-22
*
More precise numbers about Benjamin's fix for the VM.
Maxime Dénès
2015-04-22
*
Update CHANGES
Matthieu Sozeau
2015-04-22
*
Do not use list concatenation when gluing streams together, just mark them as...
Guillaume Melquiond
2015-04-22
*
Remove some spurious spaces in generated Makefiles.
Guillaume Melquiond
2015-04-22
*
STM: print trace on "anomaly, no safe id attached"
Enrico Tassi
2015-04-21
*
Fixing #4198 (looking for subterms also in the return clause of match).
Hugo Herbelin
2015-04-21
*
Fixing #3383 (a "return" clause without an "in" clause is not enough
Hugo Herbelin
2015-04-21
*
Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument
Hugo Herbelin
2015-04-21
*
Some dead code.
Hugo Herbelin
2015-04-21
*
Remove spurious ".v" from warning message.
Guillaume Melquiond
2015-04-20
*
Change magic numbers.
Matthieu Sozeau
2015-04-20
*
Inlining "fun" and "forall" tokens in parser, so that alternative notations for
Hugo Herbelin
2015-04-20
*
Slightly more efficient implementation of the logic monad.
Pierre-Marie Pédrot
2015-04-19
*
8.5beta2 release.
Matthieu Sozeau
2015-04-17
*
Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several
Hugo Herbelin
2015-04-17
*
Fixing a few typos + some uniformization of writing in doc.
Hugo Herbelin
2015-04-17
*
No longer add dev/ to the LoadPath, only to the ML path.
Guillaume Melquiond
2015-04-17
*
Ensuring purity of datastructures in the API.
Pierre-Marie Pédrot
2015-04-16
*
Test for bug #4190.
Pierre-Marie Pédrot
2015-04-16
*
Fixing bug #4190.
Pierre-Marie Pédrot
2015-04-16
*
configure: fix paths on cygwin
Enrico Tassi
2015-04-16
*
Remove dirty debug printing from funind.
Maxime Dénès
2015-04-15
*
Documenting the recommandation of toplevel-only commands.
Pierre-Marie Pédrot
2015-04-15
*
Function now supports puniveres
jforest
2015-04-14
*
better debug in recdef
jforest
2015-04-14
*
Cleaning up the implementation of search entries in Hints.
Pierre-Marie Pédrot
2015-04-14
*
Opaque implementation of auto tactics.
Pierre-Marie Pédrot
2015-04-14
*
correction of a bug reported by Tristan Crolard
jforest
2015-04-13
*
Program: Do not reduce obligation types preemptively, only at
Matthieu Sozeau
2015-04-13
*
Remove declarations of matched variables in change as an extension of
Matthieu Sozeau
2015-04-13
*
More documented representation of hint objects.
Pierre-Marie Pédrot
2015-04-13
*
Fixing bug #4186.
Pierre-Marie Pédrot
2015-04-13
*
Making the hint entry type opaque.
Pierre-Marie Pédrot
2015-04-12
*
Fix compilation broken by Matthieu's last commit.
Pierre Letouzey
2015-04-10
[next]