aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/test
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-06-17Cleanup in subtac_cases, preparing to use improvements on return predicatemsozeau
2008-02-08Backport code from command.ml to subtac_command.ml for defininingmsozeau
2007-08-26Fix de Bruijn bug in wf definitions.msozeau
2007-04-17Correct implementation of undo in obligations handling code, correct some bug...msozeau
2007-03-26Make multiple patterns work again with Program while simplifying the code.msozeau
2007-03-13Solve obligation handling bug of trying to solve automatically at Next Obliga...msozeau
2007-02-23Debug wellfounded defs, work on cleaning obls envsmsozeau
2007-02-01Abbreviation of order notation.msozeau
2007-01-29Various fixes in subtac, update some test cases.msozeau
2007-01-24Update some tests and fix section bug.msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:46:45 +0000