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