| Commit message (Expand) | Author | Age |
* | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin | 2008-06-10 |
* | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
* | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin | 2008-04-25 |
* | 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 |