| Age | Commit message (Expand) | Author |
|---|
| 2004-12-06 | Uniformisation du nom d'entrée openconstr en le nom du type open_constr | herbelin |
| 2004-12-06 | Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti... | herbelin |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-07-16 | Suppression quotify | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-06-29 | moved instantiate binding to extratactics | corbinea |
| 2004-06-28 | more evar stuff | corbinea |
| 2004-03-02 | Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va... | herbelin |
| 2004-03-01 | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin |
| 2004-01-27 | Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ... | herbelin |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-25 | Uniformisation des politiques de nommage de NewDestruct sur arguments recursi... | herbelin |
| 2003-11-17 | New tactics : econstructor, eleft, eright, esplit | clrenard |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-11-09 | Traduction semantique des InHyp de clause en InHypValue si local def | herbelin |
| 2003-11-06 | Added Instantiate ... in | corbinea |
| 2003-10-10 | Cablage en dur de inversion | herbelin |
| 2003-10-10 | changement nouvelle syntaxe (pt fixes) | barras |
| 2003-09-12 | Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c... | herbelin |
| 2003-06-19 | Ajout 'Symmetry in Hyp' | herbelin |
| 2003-06-13 | Utilisation de intro_pattern dans NewDestruct/NewInduction | herbelin |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-31 | Bug pattern_occ_hyp_list | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2002-12-21 | Légère amélioration des messages d'erreur des with-bindings et des Rewrite | herbelin |
| 2002-12-09 | Ajout Simpl et Change sur des sous-termes | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-10-21 | Ajout d'un suffixe "as [ names ]" pour nommer manuellement les | herbelin |
| 2002-10-21 | NewDestruct/NewInduction acceptent l'option "using" | herbelin |
| 2002-05-30 | Finalement un seul constr pour l'instant dans ExtraRedExpr | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-03-19 | Ajout de l'entrée ne_constrarg_list | delahaye |
| 2002-02-01 | Ajout tactiques Rename et Pose; modifications pour Inversion | herbelin |
| 2002-01-31 | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring |
| 2001-12-13 | compat ocaml 3.03 | filliatr |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-05 | Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle... | herbelin |
| 2001-09-20 | Transparent | barras |
| 2001-09-14 | Ajout syntaxe "Assert H:T." | herbelin |
| 2001-08-28 | Remplace numarg -> pure_numarg dans Double Induction | mohring |
| 2001-08-10 | Parsing | herbelin |
| 2001-08-08 | Renommage TrueCut -> Assert | herbelin |
| 2001-08-07 | Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ... | herbelin |
| 2001-08-05 | Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction | herbelin |
| 2001-07-02 | Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute... | herbelin |
| 2001-06-25 | Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ... | herbelin |
