| Commit message (Expand) | Author | Age |
|---|
| * | Bugs, nettoyage, et améliorations diverses |  herbelin | 2008-04-13 |
| * | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin | 2008-04-01 |
| * | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) |  letouzey | 2008-03-07 |
| * | Factorisation des opérations sur le type option de Util dans un module |  aspiwack | 2007-12-05 |
| * | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin | 2007-10-03 |
| * | extension of the rename tactic: the following is now allowed: | letouzey | 2007-07-06 |
| * | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin | 2007-05-22 |
| * | - Propagation des evars non résolues vers les with_bindings; permet par exemple | herbelin | 2007-05-20 |
| * | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
| * | Changement dans le kernel : |  bgregoir | 2006-12-11 |
| * | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin | 2006-05-30 |
| * | Standardisation nom option_app en option_map | herbelin | 2006-04-27 |
| * | - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses | herbelin | 2006-01-16 |
| * | Added 'clear - id' to clear all hypotheses except the ones dependent in the s... | herbelin | 2005-03-07 |
| * | COMMITED BYTECODE COMPILER |  barras | 2004-10-20 |
| * | Nouvelle en-tête | herbelin | 2004-07-16 |
| * | more evar stuff |  corbinea | 2004-06-28 |
| * | effective evar refining | corbinea | 2004-06-26 |
| * | Déplacement définition intro_pattern_expr dans Genarg | herbelin | 2004-03-01 |
| * | bugs avec Pose et Assert | barras | 2004-01-09 |
| * | factorisation et generalisation des clauses | barras | 2003-11-13 |
| * | Added Instantiate ... in | corbinea | 2003-11-06 |
| * | changement nouvelle syntaxe (pt fixes) | barras | 2003-10-10 |
| * | Ajout 'Symmetry in Hyp' | herbelin | 2003-06-19 |
| * | Utilisation de intro_pattern dans NewDestruct/NewInduction | herbelin | 2003-06-13 |
| * | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin | 2003-05-21 |
| * | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
| * | *** empty log message *** | barras | 2003-03-12 |
| * | Un type "standardisé" pour new_hyp | herbelin | 2003-01-25 |
| * | Ajout Simpl et Change sur des sous-termes | herbelin | 2002-12-09 |
| * | Réforme de l'interprétation des termes : | herbelin | 2002-11-14 |
| * | Ajout d'un suffixe "as [ names ]" pour nommer manuellement les | herbelin | 2002-10-21 |
| * | NewDestruct/NewInduction acceptent l'option "using" | herbelin | 2002-10-21 |
| * | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
| * | Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ... | herbelin | 2001-06-25 |
| * | entetes |  filliatr | 2001-03-15 |
| * | Ajout du langage de tactiques |  delahaye | 2000-05-03 |
| * | Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations | filliatr | 1999-11-24 |
| * | modules Indrec, Tacentries, Hiddentac | filliatr | 1999-11-23 |
herbelin
letouzey
aspiwack
bgregoir
barras
corbinea
filliatr
delahaye