aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/test
AgeCommit message (Expand)Author
2007-01-15Various subtac fixes.msozeau
2006-12-22Default tactic for solving goals.msozeau
2006-12-14Reimplemented equality generation for pattern matching at typing time. First ...msozeau
2006-12-12Subtac: work on cases.msozeau
2006-12-08Subtac bug fix, add list take example.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-11-16Work on dep types pattern matchingmsozeau
2006-11-15Some usability enhancements.msozeau
2006-11-10Work on mutual defs, various bug fixes.msozeau
2006-11-10Work on pattern inequalities for pattern matching branches.msozeau
2006-09-28Add dependent list combinators test.msozeau
2006-06-23Fix wrong order of existentials in eterm.msozeau
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-14Test files for subtac.msozeau