aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2006-01-11remove warnings that were left in the directory contrib/interfacebertot
2006-01-11removes several warnings in contrib/interfacebertot
2006-01-11Résidus du traducteur v7 -> v8herbelin
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
2006-01-11Suite réorganisation des fonctions d'affichageherbelin
2006-01-11Standardisation du nom de subst_raw en subst_rawconstrherbelin
2006-01-11Résidus du traducteur v7 -> v8herbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
2006-01-11Suppression résidus code v7 et traducteurherbelin
2006-01-10Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...herbelin
2006-01-10majcoq
2006-01-10Détection var inutile par ocaml 3.09herbelin
2006-01-09majcoq
2006-01-09Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...herbelin
2006-01-08majcoq
2006-01-08Prise en compte, enfin, du contexte des types de retour de ACases et RCasesherbelin
2006-01-08Prise en compte de notations numérales définies au niveau utilisateur+ lég...herbelin
2006-01-08Prise en compte de notations numérales définies au niveau utilisateur + tra...herbelin
2006-01-08Enregistrement dans glob.dump des utilisations de notations numériques (qui ...herbelin
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...herbelin
2006-01-08Automatisation de l'utilisation de token primitifs dans les motifs de filtrageherbelin
2006-01-08Ajout rawconstr_of_aconstrherbelin
2006-01-08Fonctions de conversion rawconstr <-> cases_patternherbelin
2006-01-07majcoq
2006-01-07Réorganisation; suppression code mort; documentationherbelin
2006-01-07MAJherbelin
2006-01-06majcoq
2006-01-06Petite modification de la gestion du '.' (jmn)coq
2006-01-05majcoq
2006-01-05*** empty log message ***barras
2006-01-05Amelioration de l'elimination des preuves (bugs #1052 et #950-II) (jmn)coq
2006-01-05Test choix conflit afficheur de nombres selon la présence ou pas d'une coercionherbelin
2006-01-05*** empty log message ***coq
2006-01-05Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ...herbelin
2006-01-05Adding a man page for doqdoc (JMN)coq
2006-01-04majcoq
2006-01-04Suppression des coercions non seulement avant l'affichage des notations mais ...herbelin
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...herbelin
2006-01-04Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)herbelin
2006-01-04Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr (d...herbelin
2006-01-04Achèvement du commit incomplet de la révision 1.110 (cvs log toplevel/metas...herbelin
2006-01-03majcoq
2006-01-03Modification pour que l'ordre des éléments respecte l'ordre dans lequel ils...herbelin
2006-01-03Redéclaration de la notation à l'import pour être cohérent avec l'activat...herbelin
2006-01-02majcoq
2006-01-02Affichage de 'O' (lettre) comme '0' (chiffre)herbelin
2006-01-01majcoq
2005-12-31majcoq