| Age | Commit message (Expand) | Author |
|---|
| 2007-02-16 | lift params appropriately, do not need to coerce to tycon | msozeau |
| 2007-02-16 | Update implementation for dependent types. Works just as well as before for s... | msozeau |
| 2007-02-13 | Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de | herbelin |
| 2007-02-12 | Fix matching on dependent types, taking a safe stand. | msozeau |
| 2007-02-09 | Separate Tactics in subtac. | msozeau |
| 2007-02-08 | Add lif then else for if in bool. | msozeau |
| 2007-02-08 | Fix myinjection tactic, generalize coercion for applications | msozeau |
| 2007-02-07 | Fix mistake naming my Tactics file Tactics :) | msozeau |
| 2007-02-07 | Add tactics for induction on subterms. | msozeau |
| 2007-02-07 | Various subtac fixes. Add inequalities in pattern matching branches when need... | msozeau |
| 2007-02-03 | Work on ineqs generation. | msozeau |
| 2007-02-02 | Factorisation de la règle Constr.binder dans g_subtac.ml pour éviter | herbelin |
| 2007-02-01 | Abbreviation of order notation. | msozeau |
| 2007-01-30 | constr_of_pat bug with nested patterns. | msozeau |
| 2007-01-29 | Various fixes in subtac, update some test cases. | msozeau |
| 2007-01-29 | Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes. | msozeau |
| 2007-01-24 | Update some tests and fix section bug. | msozeau |
| 2007-01-15 | Various subtac fixes. | msozeau |
| 2007-01-08 | Subtac fixes, support for reasoning on wf defs. | msozeau |
| 2007-01-02 | Rework subtac pattern matching equalities generation. | msozeau |
| 2006-12-22 | Default tactic for solving goals. | msozeau |
| 2006-12-14 | Reimplemented equality generation for pattern matching at typing time. First ... | msozeau |
| 2006-12-12 | Subtac: work on cases. | msozeau |
| 2006-12-08 | Subtac bug fix, add list take example. | msozeau |
| 2006-11-29 | Fork of cases impl for subtac. | msozeau |
| 2006-11-20 | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin |
| 2006-11-16 | Work on dep types pattern matching | msozeau |
| 2006-11-15 | Some usability enhancements. | msozeau |
| 2006-11-13 | Better solve using tactics impl. | msozeau |
| 2006-11-10 | Work on mutual defs, various bug fixes. | msozeau |
| 2006-11-10 | Work on pattern inequalities for pattern matching branches. | msozeau |
| 2006-11-09 | Support for mutual defs in obligation handling. | msozeau |
| 2006-10-31 | Debug obligation handling code | msozeau |
| 2006-10-31 | Fix compile error | msozeau |
| 2006-10-31 | Work on obligation separation. | msozeau |
| 2006-10-29 | Suite commit polymorphisme | herbelin |
| 2006-10-26 | Facilities to automatically solve obligations | msozeau |
| 2006-10-10 | Fix 0 obligations bug | msozeau |
| 2006-09-28 | Add dependent list combinators test. | msozeau |
| 2006-09-15 | Report de l'heuristique d'unification premier ordre flexible/rigide | herbelin |
| 2006-09-04 | Fix wrong order for building library, add informative messages. | msozeau |
| 2006-09-01 | New handling of obligations. | msozeau |
| 2006-09-01 | Forgot to add this one. | msozeau |
| 2006-09-01 | Subtac fixes, new way of handling obligations in progress. | msozeau |
| 2006-06-23 | Fix wrong order of existentials in eterm. | msozeau |
| 2006-06-22 | Mutually structurally recursive defs and rec using measures added. | msozeau |
| 2006-06-20 | Wellfounded recursion using subtac working again. | msozeau |
| 2006-06-20 | Progress in new wf def typing. | msozeau |
| 2006-06-20 | Rewrite of the recursive defs handling in progress. | msozeau |
| 2006-06-07 | Correction trou de subject-reduction de create_arg dans genarg.mli | herbelin |
