| Age | Commit message (Expand) | Author |
|---|
| 2007-02-07 | Add tactics for induction on subterms. | msozeau |
| 2007-02-07 | Meilleur anglais (cf 9619) | herbelin |
| 2007-02-07 | Various subtac fixes. Add inequalities in pattern matching branches when need... | msozeau |
| 2007-02-07 | doc de ring/field + option infinite -> completeness | barras |
| 2007-02-05 | changement dans ring specification du sign, division | bgregoir |
| 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-02 | field: introduction de Get_goal | bgregoir |
| 2007-02-02 | ring: introduction de Get_goal | bgregoir |
| 2007-02-02 | Now 1/x * x simplifies to 1 | thery |
| 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-28 | "suffices" implemented + syntax cleanup | corbinea |
| 2007-01-26 | Contounement d'un probleme avec la VM dans Function | jforest |
| 2007-01-24 | Update some tests and fix section bug. | msozeau |
| 2007-01-24 | changement de la fonction norm_subst | bgregoir |
| 2007-01-23 | ring : Correction du bug PR#1306 | bgregoir |
| 2007-01-22 | Correction du bug #1315: | notin |
| 2007-01-22 | Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent | herbelin |
| 2007-01-19 | Protection contre les warnings 'unused variable' de ocaml 3.09 | herbelin |
| 2007-01-15 | Various subtac fixes. | msozeau |
| 2007-01-12 | Suite au mail de Lionel a propos du Makefile: | letouzey |
| 2007-01-12 | un saut de ligne ... | letouzey |
| 2007-01-10 | Merge from Lionel Elie Mamane's private branch: | lmamane |
| 2007-01-10 | Nouvelle approche pour le discharge modulaire | herbelin |
| 2007-01-08 | Subtac fixes, support for reasoning on wf defs. | msozeau |
| 2007-01-05 | suite de la reparation du bug 1239: apres les inds, les records et vars de types | letouzey |
| 2007-01-02 | Rework subtac pattern matching equalities generation. | msozeau |
| 2006-12-28 | Remplacement de la définition de Pind et Prec par une définition | herbelin |
| 2006-12-22 | Default tactic for solving goals. | msozeau |
| 2006-12-21 | typo malencontreuse | filliatr |
| 2006-12-17 | reparation bug 1239 | letouzey |
| 2006-12-15 | Changement dans ring et field, beaucoup de correction d'erreurs, | bgregoir |
| 2006-12-15 | contrib/dp: tactique ergo (voir ergo.lri.fr) | filliatr |
| 2006-12-14 | Reimplemented equality generation for pattern matching at typing time. First ... | msozeau |
| 2006-12-12 | Subtac: work on cases. | msozeau |
| 2006-12-11 | Changement dans le kernel : | bgregoir |
| 2006-12-08 | contrib/dp | filliatr |
| 2006-12-08 | Subtac bug fix, add list take example. | msozeau |
| 2006-11-29 | Fork of cases impl for subtac. | msozeau |
| 2006-11-24 | Functional graph merging deals with letins. | courtieu |
| 2006-11-24 | Fixed the graph merging parameter order. | courtieu |
| 2006-11-23 | Fixing syntax and parameter order in functional graph merging. | courtieu |
| 2006-11-21 | Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de | herbelin |
| 2006-11-20 | Changing merging functional scheme syntax. | courtieu |
| 2006-11-20 | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin |
| 2006-11-19 | mult_sym, plus_sym -> mult_comm, plus_comm | herbelin |
| 2006-11-16 | Small fix in functional graph merging. | courtieu |
