| Commit message (Expand) | Author | Age |
* | Retour r9310 en attendant mieux | herbelin | 2007-02-09 |
* | Separate Tactics in subtac. | msozeau | 2007-02-09 |
* | Add lif then else for if in bool. | msozeau | 2007-02-08 |
* | Fix myinjection tactic, generalize coercion for applications | msozeau | 2007-02-08 |
* | Fix mistake naming my Tactics file Tactics :) | msozeau | 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-07 |
* | changement dans ring specification du sign, division | bgregoir | 2007-02-05 |
* | Work on ineqs generation. | msozeau | 2007-02-03 |
* | 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-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 |