| Commit message (Expand) | Author | Age |
* | modif des fixpoints pour que si on donne une notation au produit, les pts fix... | barras | 2004-03-05 |
* | ide: silent behavior better, save icon, -byte works | marche | 2004-03-03 |
* | Traduction 'Cases' en pattern-matching | herbelin | 2004-02-28 |
* | Eviter la stricte redondance de regles de grammaires v7 | herbelin | 2004-02-28 |
* | Keep structure information for Fixpoint declaration and Fix terms | bertot | 2004-02-26 |
* | - fixed the Assert_failure error in kernel/modops | barras | 2004-02-18 |
* | Ajout de lconstr, constr et binder_constr dans Print Grammar constr | herbelin | 2004-02-17 |
* | Correction d'un pb '{ _ }' et uniformisation du comportement de Notation et R... | herbelin | 2004-02-13 |
* | Localisation des erreurs d'internalisation des notations de tactiques | herbelin | 2004-02-12 |
* | Localisation des erreurs d'internalisation des notations de tactiques | herbelin | 2004-02-12 |
* | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin | 2004-02-12 |
* | Boite autour des quote pour eviter un retour a la ligne apres le premier guil... | herbelin | 2004-02-04 |
* | search window | coq | 2004-02-04 |
* | Bug focus | herbelin | 2004-02-03 |
* | Protection contre noms de variable indefinis et guillemets autour des constr | herbelin | 2004-02-03 |
* | Ajout option raw_print (Set Printing All) pour desactiver toute fonctionnalit... | herbelin | 2004-01-29 |
* | Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :... | herbelin | 2004-01-29 |
* | reparation de qqs bugs du traducteur | barras | 2004-01-26 |
* | Protection table des locations lors de Load (pour coqdoc) | herbelin | 2004-01-22 |
* | Export information des references de notations pour coqdoc | herbelin | 2004-01-21 |
* | Ajout nouvelles options | herbelin | 2004-01-15 |
* | Ajout load-vernac-source-verbose | herbelin | 2004-01-15 |
* | Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a... | herbelin | 2004-01-13 |
* | bugs avec Pose et Assert | barras | 2004-01-09 |
* | Defaut d'information affichage en cas de notation incompatible | herbelin | 2004-01-05 |
* | meilleure presentation des commentaires du traducteur | barras | 2004-01-02 |
* | ameliorations coqide | coq | 2003-12-30 |
* | *** empty log message *** | barras | 2003-12-24 |
* | MAJ messages d'erreurs en accord avec la doc | herbelin | 2003-12-20 |
* | Bug rattrapage erreur locate_reference | herbelin | 2003-12-20 |
* | Suppression de l'espace avant les notations commencant par un ident | herbelin | 2003-12-19 |
* | option -n de coq-tex | marche | 2003-12-12 |
* | Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7... | herbelin | 2003-11-29 |
* | Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7... | herbelin | 2003-11-29 |
* | Utilisation nom dans message d'erreur implicite pas trouve | herbelin | 2003-11-29 |
* | Monstrueuse inefficacite due a l'innocence du redacteur de la ligne vis a vis... | herbelin | 2003-11-27 |
* | Traitement plus clair, notamment pour Locate, de quand quoter les composantes... | herbelin | 2003-11-22 |
* | MAJ format et doc | herbelin | 2003-11-21 |
* | Bug: faut brancher la sortie des tactiques sur stdout pendant traduction | herbelin | 2003-11-18 |
* | Utilisation de la date cvs dans l'en-tete si make.result existe | herbelin | 2003-11-18 |
* | Bug v8 (regles connues etaient re-enregistrees) + tables dans egrammar | herbelin | 2003-11-15 |
* | Ajout Print Implicit avec depliage du type | herbelin | 2003-11-15 |
* | Check bavard meme en mode silencieux, car on l'a voulu | herbelin | 2003-11-14 |
* | Prise en compte des alias syntaxiques vers des references dans divers lieux d... | herbelin | 2003-11-12 |
* | Idtac peut prendre un argument à afficher | narboux | 2003-11-12 |
* | petits changements de syntaxe | barras | 2003-11-12 |
* | Re-suppression de is_verbose dans Print, pour coqide | herbelin | 2003-11-10 |
* | Suppression SearchNamed finalement redondant avec SearchAbout | herbelin | 2003-11-10 |
* | Mise en place traduction des tactiques apres evaluation pour permettre des ch... | herbelin | 2003-11-09 |
* | Fusion de tuple_constr/tuple_pattern dans operconstr/pattern | herbelin | 2003-11-08 |