index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
subtac
/
subtac_utils.mli
Age
Commit message (
Expand
)
Author
2007-01-15
Various subtac fixes.
msozeau
2006-12-14
Reimplemented equality generation for pattern matching at typing time. First ...
msozeau
2006-12-12
Subtac: work on cases.
msozeau
2006-11-29
Fork of cases impl for subtac.
msozeau
2006-11-16
Work on dep types pattern matching
msozeau
2006-11-10
Work on mutual defs, various bug fixes.
msozeau
2006-10-31
Debug obligation handling code
msozeau
2006-10-26
Facilities to automatically solve obligations
msozeau
2006-09-01
New handling of obligations.
msozeau
2006-09-01
Subtac fixes, new way of handling obligations in progress.
msozeau
2006-06-22
Mutually structurally recursive defs and rec using measures added.
msozeau
2006-06-20
Wellfounded recursion using subtac working again.
msozeau
2006-06-20
Rewrite of the recursive defs handling in progress.
msozeau
2006-06-01
Fix some nasty bug with the evars-to-dependent sum encoding.
msozeau
2006-05-29
The "clean integration of subtac" patch.
msozeau
2006-04-10
Actual fix for the unification problem in theories/Reals/Rtrigo_fun (previous...
msozeau
2006-04-07
- Documentation of the Program tactics.
msozeau
2006-03-22
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
