| Age | Commit message (Expand) | Author |
|---|
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-01 | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-02 | Extension to the general sequence operator (tactical). Now in addition to ... | emakarov |
| 2006-03-22 | Made pretyping a functor over a coercion implementation. Pretyping.Default us... | msozeau |
| 2006-01-21 | Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f... | herbelin |
| 2006-01-11 | removes several warnings in contrib/interface | bertot |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-03-07 | Added 'clear - id' to clear all hypotheses except the ones dependent in the s... | herbelin |
| 2005-02-18 | Standardisation of function names about global references (especially, renami... | herbelin |
| 2004-07-18 | Abstraction vis a vis du type loc pour ocaml 3.08 | herbelin |
| 2004-02-16 | corrects a bug in name reservation, simplifies or_intro, removes dead code | bertot |
| 2004-02-11 | a new version that uses intro patterns, but the code still needs some cleaning | bertot |
| 2003-11-13 | factorisation et generalisation des clauses | barras |
| 2003-11-12 | Bug TacId | herbelin |
| 2003-10-13 | Deplacement next_global_ident_away dans Termops | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-06-10 | Ajout notation c.(f) en v8 pour les projections de Record | herbelin |
| 2003-05-21 | Suppression définitive de lmatch et or_metanum dans tacinterp | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-31 | factorisation des "constant" dans les contrib/* ( maintenant dans coqlib ) | corbinea |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-01-24 | Corrects the way conjunctions, existential quantifications, and arrows are | bertot |
| 2003-01-23 | Make proof by pointing work for the new notations of existential quantification. | bertot |
| 2003-01-22 | removes all references to ctast.ml the Makefile has been updated accordingly. | bertot |
| 2002-12-21 | Légère amélioration des messages d'erreur des with-bindings et des Rewrite | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-09-24 | Un peu (plus) d'ordre dans Nametab... | coq |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2001-12-18 | Integrating the Ltac language and the Blast tool into the interface | bertot |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-17 | Abstraction de l'immplementation de dirpath et implementation dans l'autre se... | herbelin |
| 2001-10-12 | reparation | filliatr |
| 2001-08-10 | Prsing | herbelin |
| 2001-04-07 | Two constants had been given in the wrong package (Logic_type instead of | bertot |
| 2001-04-04 | Files that handle the dialogue with the graphical user-interface pcoq. | bertot |
