index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
subtac
/
subtac_utils.mli
Commit message (
Expand
)
Author
Age
*
Fix some bugs, add possibility of automatically solving a proof statement's o...
msozeau
2007-10-24
*
Move Program tactics into a proper theories/ directory as they are general pu...
msozeau
2007-08-07
*
Cleanup, use Util list functions when possible
msozeau
2007-07-12
*
Better handling of aliases, add command to solve a particular obligation.
msozeau
2007-07-02
*
Support for implicit formal argument types in Program ; parse types in type s...
msozeau
2007-03-28
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Debug wellfounded defs, work on cleaning obls envs
msozeau
2007-02-23
*
Various little subtac fixes, add some useful tactics.
msozeau
2007-02-19
*
Update implementation for dependent types. Works just as well as before for s...
msozeau
2007-02-16
*
Various subtac fixes. Add inequalities in pattern matching branches when need...
msozeau
2007-02-07
*
Various fixes in subtac, update some test cases.
msozeau
2007-01-29
*
Various subtac fixes.
msozeau
2007-01-15
*
Reimplemented equality generation for pattern matching at typing time. First ...
msozeau
2006-12-14
*
Subtac: work on cases.
msozeau
2006-12-12
*
Fork of cases impl for subtac.
msozeau
2006-11-29
*
Work on dep types pattern matching
msozeau
2006-11-16
*
Work on mutual defs, various bug fixes.
msozeau
2006-11-10
*
Debug obligation handling code
msozeau
2006-10-31
*
Facilities to automatically solve obligations
msozeau
2006-10-26
*
New handling of obligations.
msozeau
2006-09-01
*
Subtac fixes, new way of handling obligations in progress.
msozeau
2006-09-01
*
Mutually structurally recursive defs and rec using measures added.
msozeau
2006-06-22
*
Wellfounded recursion using subtac working again.
msozeau
2006-06-20
*
Rewrite of the recursive defs handling in progress.
msozeau
2006-06-20
*
Fix some nasty bug with the evars-to-dependent sum encoding.
msozeau
2006-06-01
*
The "clean integration of subtac" patch.
msozeau
2006-05-29
*
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-10
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Subtac fixes, single fixpoint definitions are working again. Added a toggle o...
msozeau
2006-03-22
*
Made pretyping a functor over a coercion implementation. Pretyping.Default us...
msozeau
2006-03-22