aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/test
Commit message (Expand)AuthorAge
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
* Fix de Bruijn bug in wf definitions.Gravatar msozeau2007-08-26
* Correct implementation of undo in obligations handling code, correct some bug...Gravatar msozeau2007-04-17
* Make multiple patterns work again with Program while simplifying the code.Gravatar msozeau2007-03-26
* Solve obligation handling bug of trying to solve automatically at Next Obliga...Gravatar msozeau2007-03-13
* Debug wellfounded defs, work on cleaning obls envsGravatar msozeau2007-02-23
* Abbreviation of order notation.Gravatar msozeau2007-02-01
* Various fixes in subtac, update some test cases.Gravatar msozeau2007-01-29
* Update some tests and fix section bug.Gravatar msozeau2007-01-24
* Various subtac fixes.Gravatar msozeau2007-01-15
* Default tactic for solving goals.Gravatar msozeau2006-12-22
* Reimplemented equality generation for pattern matching at typing time. First ...Gravatar msozeau2006-12-14
* Subtac: work on cases.Gravatar msozeau2006-12-12
* Subtac bug fix, add list take example.Gravatar msozeau2006-12-08
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* Work on dep types pattern matchingGravatar msozeau2006-11-16
* Some usability enhancements.Gravatar msozeau2006-11-15
* Work on mutual defs, various bug fixes.Gravatar msozeau2006-11-10
* Work on pattern inequalities for pattern matching branches.Gravatar msozeau2006-11-10
* Add dependent list combinators test.Gravatar msozeau2006-09-28
* Fix wrong order of existentials in eterm.Gravatar msozeau2006-06-23
* Mutually structurally recursive defs and rec using measures added.Gravatar msozeau2006-06-22
* Rewrite of the recursive defs handling in progress.Gravatar msozeau2006-06-20
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
* Test files for subtac.Gravatar msozeau2006-04-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 16:24:59 +0000