index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
subtac
Commit message (
Expand
)
Author
Age
*
Use a lazy value for the message in FailError, so that it won't be
msozeau
2009-06-11
*
Fix implicit args code so that declarations are added for all
msozeau
2009-05-27
*
Fix de Bruijn lifting bug appearing when we match on multiple terms with
msozeau
2009-05-26
*
Support for definition hooks in subtac.
msozeau
2009-05-16
*
More efficient handling of evars in Program Fixpoint commands.
msozeau
2009-04-28
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
- New cleaning phase for the entry points of pretyping.ml
herbelin
2009-04-24
*
Better Requires in Classes. Fix bug #2093: the code does not require
msozeau
2009-04-16
*
Experimental support for automatic destruction of recursive calls and
msozeau
2009-04-08
*
Fix bug #2083 for good: verify that the measure and relation are
msozeau
2009-04-08
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Fixes in Program:
msozeau
2009-04-07
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
Fixes in Program well-founded definitions:
msozeau
2009-03-26
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20