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