| Commit message (Expand) | Author | Age |
* | ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien... | herbelin | 2004-12-29 |
* | Restauration type casted_open_constr pour tactique refine car l'unification n... | herbelin | 2004-12-09 |
* | 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-12-06 |
* | COMMITED BYTECODE COMPILER | barras | 2004-10-20 |
* | Suppression quotify | herbelin | 2004-07-16 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | moved instantiate binding to extratactics | corbinea | 2004-06-29 |
* | more evar stuff | corbinea | 2004-06-28 |
* | Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va... | herbelin | 2004-03-02 |
* | Généralisation du type ltac Identifier en IntroPattern; prise en compte des... | herbelin | 2004-03-01 |
* | Ajout 'as (x,...,y)' dans NewDestruct et NewInd, NewInduction, ... | herbelin | 2004-01-27 |
* | bugs avec Pose et Assert | barras | 2004-01-09 |
* | meilleure presentation des commentaires du traducteur | barras | 2004-01-02 |
* | Nouvelle tactique EExists | clrenard | 2003-12-01 |
* | Uniformisation des politiques de nommage de NewDestruct sur arguments recursi... | herbelin | 2003-11-25 |
* | New tactics : econstructor, eleft, eright, esplit | clrenard | 2003-11-17 |
* | factorisation et generalisation des clauses | barras | 2003-11-13 |
* | Traduction semantique des InHyp de clause en InHypValue si local def | herbelin | 2003-11-09 |
* | Added Instantiate ... in | corbinea | 2003-11-06 |
* | Cablage en dur de inversion | herbelin | 2003-10-10 |
* | changement nouvelle syntaxe (pt fixes) | barras | 2003-10-10 |
* | Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c... | herbelin | 2003-09-12 |
* | 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 |
* | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin | 2003-05-19 |
* | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin | 2003-04-07 |
* | Bug pattern_occ_hyp_list | herbelin | 2003-03-31 |
* | *** empty log message *** | barras | 2003-03-12 |
* | Légère amélioration des messages d'erreur des with-bindings et des Rewrite | herbelin | 2002-12-21 |
* | 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 |
* | Finalement un seul constr pour l'instant dans ExtraRedExpr | herbelin | 2002-05-30 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | Ajout de l'entrée ne_constrarg_list | delahaye | 2002-03-19 |
* | Ajout tactiques Rename et Pose; modifications pour Inversion | herbelin | 2002-02-01 |
* | changement generation de schema d'elimination, False_rec est primitif, Constr... | mohring | 2002-01-31 |
* | compat ocaml 3.03 | filliatr | 2001-12-13 |
* | GROS COMMIT: | barras | 2001-11-05 |
* | Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle... | herbelin | 2001-10-05 |
* | Transparent | barras | 2001-09-20 |
* | Ajout syntaxe "Assert H:T." | herbelin | 2001-09-14 |
* | Remplace numarg -> pure_numarg dans Double Induction | mohring | 2001-08-28 |
* | Parsing | herbelin | 2001-08-10 |
* | Renommage TrueCut -> Assert | herbelin | 2001-08-08 |
* | Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ... | herbelin | 2001-08-07 |
* | Mise en place d'un nouveau Destruct sur le modèle du nouvel Induction | herbelin | 2001-08-05 |