| Commit message (Expand) | Author | Age |
|---|
| * | ring: introduction de Get_goal |  bgregoir | 2007-02-02 |
| * | Now 1/x * x simplifies to 1 |  thery | 2007-02-02 |
| * | Abbreviation of order notation. |  msozeau | 2007-02-01 |
| * | constr_of_pat bug with nested patterns. | msozeau | 2007-01-30 |
| * | 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-29 |
| * | "suffices" implemented + syntax cleanup |  corbinea | 2007-01-28 |
| * | Contounement d'un probleme avec la VM dans Function |  jforest | 2007-01-26 |
| * | Update some tests and fix section bug. | msozeau | 2007-01-24 |
| * | changement de la fonction norm_subst | bgregoir | 2007-01-24 |
| * | ring : Correction du bug PR#1306 | bgregoir | 2007-01-23 |
| * | Correction du bug #1315: |  notin | 2007-01-22 |
| * | Error au lieu de anomaly si les appels à simplify, harvey, zenon, ... échouent |  herbelin | 2007-01-22 |
| * | Protection contre les warnings 'unused variable' de ocaml 3.09 | herbelin | 2007-01-19 |
| * | Various subtac fixes. | msozeau | 2007-01-15 |
| * | Suite au mail de Lionel a propos du Makefile: |  letouzey | 2007-01-12 |
| * | un saut de ligne ... | letouzey | 2007-01-12 |
| * | Merge from Lionel Elie Mamane's private branch: |  lmamane | 2007-01-10 |
| * | Nouvelle approche pour le discharge modulaire | herbelin | 2007-01-10 |
| * | Subtac fixes, support for reasoning on wf defs. | msozeau | 2007-01-08 |
| * | suite de la reparation du bug 1239: apres les inds, les records et vars de types | letouzey | 2007-01-05 |
| * | Rework subtac pattern matching equalities generation. | msozeau | 2007-01-02 |
| * | Remplacement de la définition de Pind et Prec par une définition | herbelin | 2006-12-28 |
| * | Default tactic for solving goals. | msozeau | 2006-12-22 |
| * | typo malencontreuse |  filliatr | 2006-12-21 |
| * | reparation bug 1239 | letouzey | 2006-12-17 |
| * | 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-15 |
| * | Reimplemented equality generation for pattern matching at typing time. First ... | msozeau | 2006-12-14 |
| * | Subtac: work on cases. | msozeau | 2006-12-12 |
| * | Changement dans le kernel : | bgregoir | 2006-12-11 |
| * | contrib/dp | filliatr | 2006-12-08 |
| * | Subtac bug fix, add list take example. | msozeau | 2006-12-08 |
| * | Fork of cases impl for subtac. | msozeau | 2006-11-29 |
| * | Functional graph merging deals with letins. |  courtieu | 2006-11-24 |
| * | Fixed the graph merging parameter order. | courtieu | 2006-11-24 |
| * | Fixing syntax and parameter order in functional graph merging. | courtieu | 2006-11-23 |
| * | Nettoyage de l'utilisation de l'expansion des macros ~ et $ dans les noms de | herbelin | 2006-11-21 |
| * | Changing merging functional scheme syntax. | courtieu | 2006-11-20 |
| * | Suppression du type 'tac dans les abstract_argument_type: devenu inutile | herbelin | 2006-11-20 |
| * | mult_sym, plus_sym -> mult_comm, plus_comm | herbelin | 2006-11-19 |
| * | Small fix in functional graph merging. | courtieu | 2006-11-16 |
| * | suppression de code mort (avec bug de nom) | letouzey | 2006-11-16 |
| * | pb avec r9379 + modifs dans ring |  barras | 2006-11-16 |
| * | Work on dep types pattern matching | msozeau | 2006-11-16 |
| * | suite de r9362: reconnaissance de qqs injections entre nat, N et Z | barras | 2006-11-16 |
| * | Some usability enhancements. | msozeau | 2006-11-15 |
| * | Better solve using tactics impl. | msozeau | 2006-11-13 |
| * | Correction de la seconde partie du bug #1278 | jforest | 2006-11-13 |
| * | Correction de la premiere partie du #1278 (but non referme en cas d'echec) | jforest | 2006-11-13 |
bgregoir
thery
msozeau
corbinea
jforest
notin
herbelin
letouzey
lmamane
filliatr
courtieu
barras