aboutsummaryrefslogtreecommitdiff
path: root/contrib/subtac/Utils.v
AgeCommit message (Expand)Author
2007-06-14Add Solve All Obligations command, fix bug in inequality generation introduce...msozeau
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...msozeau
2007-04-17Correct implementation of undo in obligations handling code, correct some bug...msozeau
2007-03-20Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a...msozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-11Remove bugguy notationsmsozeau
2007-03-08Create a program_scope in subtac Utilsmsozeau
2007-02-19Various little subtac fixes, add some useful tactics.msozeau
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
2007-02-09Separate Tactics in subtac.msozeau
2007-02-08Add lif then else for if in bool.msozeau
2007-02-08Fix myinjection tactic, generalize coercion for applicationsmsozeau
2007-02-07Add tactics for induction on subterms.msozeau
2007-02-07Various subtac fixes. Add inequalities in pattern matching branches when need...msozeau
2007-01-29Various fixes in subtac, update some test cases.msozeau
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
2007-01-24Update some tests and fix section bug.msozeau
2007-01-15Various subtac fixes.msozeau
2007-01-08Subtac fixes, support for reasoning on wf defs.msozeau
2006-12-08Subtac bug fix, add list take example.msozeau
2006-11-29Fork of cases impl for subtac.msozeau
2006-10-26Facilities to automatically solve obligationsmsozeau
2006-09-01New handling of obligations.msozeau
2006-06-20Progress in new wf def typing.msozeau
2006-05-29The "clean integration of subtac" patch.msozeau
2006-04-10Fixes for new unification, not used in default version as it really changes u...msozeau
2006-04-07- Documentation of the Program tactics.msozeau