aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/g_subtac.ml4
Commit message (Expand)AuthorAge
* Solve obligation handling bug of trying to solve automatically at Next Obliga...Gravatar msozeau2007-03-13
* Various subtac fixes. Add inequalities in pattern matching branches when need...Gravatar msozeau2007-02-07
* Factorisation de la règle Constr.binder dans g_subtac.ml pour éviterGravatar herbelin2007-02-02
* Various subtac fixes.Gravatar msozeau2007-01-15
* Subtac fixes, support for reasoning on wf defs.Gravatar msozeau2007-01-08
* Fork of cases impl for subtac.Gravatar msozeau2006-11-29
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Some usability enhancements.Gravatar msozeau2006-11-15
* Work on obligation separation.Gravatar msozeau2006-10-31
* New handling of obligations.Gravatar msozeau2006-09-01
* Subtac fixes, new way of handling obligations in progress.Gravatar msozeau2006-09-01
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 06:33:41 +0000