| Age | Commit message (Expand) | Author |
|---|
| 2005-12-26 | Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*... | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-21 | Restructuration des points d'entrée de Pretyping et Constrintern | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-01-02 | Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p... | herbelin |
| 2004-12-29 | ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien... | herbelin |
| 2004-12-24 | Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque... | herbelin |
| 2004-12-01 | pp of nested fixpoints (dangling with/for) | barras |
| 2004-11-04 | Affichage des univers | herbelin |
| 2004-10-20 | COMMITED BYTECODE COMPILER | barras |
| 2004-09-09 | Ajout de or-pattern pour le match-with v8 | herbelin |
| 2004-07-16 | Abstraction vis à vis du type loc pour compatibilité ocaml 3.08 | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-04-17 | pb facto des Fixpoint + erreur avec -dump-glob et Load | barras |
| 2004-04-08 | Chgt role 2eme argument AList et implantation affichage motifs recursifs de n... | herbelin |
| 2004-03-17 | Mise en place de motifs récursifs dans Notation; quelques simplifications au... | herbelin |
| 2004-03-12 | Bug inversion abstract_constr_expr et prod_constr_expr | herbelin |
| 2004-03-05 | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras |
| 2004-02-26 | Keep structure information for Fixpoint declaration and Fix terms | bertot |
| 2004-02-20 | commit précédent erroné | herbelin |
| 2004-02-19 | Bugs/insuffisances trouvees en traduisant MMode | herbelin |
| 2004-02-18 | - fixed the Assert_failure error in kernel/modops | barras |
| 2004-01-26 | reparation de qqs bugs du traducteur | barras |
| 2004-01-09 | bugs avec Pose et Assert | barras |
| 2004-01-05 | certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles | barras |
| 2004-01-02 | meilleure presentation des commentaires du traducteur | barras |
| 2003-12-23 | Finalement, espacement autour du ':' pour a la fois exists, forall et fun | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-15 | Protection du nom Eval pour eviter conflit avec Eval in | herbelin |
| 2003-12-03 | Rle_monotony_contra devenu Rmult_le_reg_l avant traduction | herbelin |
| 2003-11-29 | Renommages de variables dans RIneq | herbelin |
| 2003-11-19 | ajout de Znumtheory.v dans ZArith | letouzey |
| 2003-11-19 | Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans... | herbelin |
| 2003-11-18 | reparation bug moins unaire (erreur de PP) | barras |
| 2003-11-14 | Automatisation de la traduction de iff_trans; renommage IF | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-12 | Mise en place systeme de renommage des noms de variables liees dans la biblio... | herbelin |
| 2003-11-12 | petits changements de syntaxe | barras |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que | herbelin |
| 2003-10-30 | Affichage des negatifs au niveau de l'application, et des positifs au dessus ... | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-21 | Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par... | herbelin |
| 2003-10-16 | lettac -> set | barras |
| 2003-10-10 | Ajout printers pour constr et constr_pattern (sans traduction) | herbelin |
| 2003-10-10 | changement nouvelle syntaxe (pt fixes) | barras |
| 2003-10-08 | Des abbreviations pour constrintern.ml | herbelin |
| 2003-10-02 | as au niveau de app | herbelin |
| 2003-09-26 | Syntaxe plus liberale pour le type des arguments de filtrage du 'match' | herbelin |
| 2003-09-22 | traducteur: affiche les commentaires a l'interieur des commandes | barras |
| 2003-09-21 | Mise en place d'implicites par noms en v8 | herbelin |
