aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* Bug affichage coercionsGravatar herbelin2001-02-16
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Tentative d'amélioration affichage decls localesGravatar herbelin2001-02-16
* Suppression sp_of_idGravatar herbelin2001-02-16
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Prise en compte noms longs dans ImplicitsGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...Gravatar herbelin2001-02-14
* Bug nommage StdlibGravatar herbelin2001-02-13
* Bug nombres en chiffres décimaux dans les CasesGravatar herbelin2001-02-12
* Bug point final dans la syntaxe theorem_bodyGravatar herbelin2001-02-09
* exported a few functions that are used in graphical interface pcoq.Gravatar bertot2001-02-09
* Several pairs of different functions actually had the same name, soGravatar bertot2001-02-09
* modif de la syntax: assoc a droite pour RingGravatar mayero2001-02-08
* SimplificationsGravatar herbelin2001-02-08
* Modif pour les patterns de sous-termesGravatar delahaye2001-02-07
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
* Ajout d'une commande pour afficher chaque coercion à la demandeGravatar herbelin2001-02-06
* Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...Gravatar herbelin2001-02-06
* Extension coerce_to_varGravatar herbelin2001-02-05
* Restructuration de classops; évolution en une version mieux intégrée au re...Gravatar herbelin2001-02-05
* Restructuration de classops; évolution en une version mieux intégrée au re...Gravatar herbelin2001-02-05
* Correction pour Time pour ne pas etre oblige de mettre deux pointsGravatar delahaye2001-02-05
* *** empty log message ***Gravatar mohring2001-02-01
* Bug localisation des Syntactif DefinitionGravatar herbelin2001-01-31
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Ajout option Set/Unset/Test Printing CoercionsGravatar herbelin2001-01-31
* backtrack sur le lexeur de la V6Gravatar filliatr2001-01-30
* Simplification ImpargsGravatar herbelin2001-01-27
* Factorisation du '.' finalGravatar herbelin2001-01-27
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les CoercionsGravatar herbelin2001-01-24
* Ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Prise en compte de constructeurs qualifiés dans les patternsGravatar herbelin2001-01-19
* Nouveau module pour centraliser les chemins des constantes globales utilisée...Gravatar herbelin2001-01-19
* Ajout d'un parseur d'entiers sous forme de patternGravatar herbelin2001-01-19
* Autour des quotations avec CasesGravatar herbelin2001-01-19
* Réparation bug extensibilité de Constr.patternGravatar herbelin2001-01-19
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
* bug head_pattern_boundGravatar herbelin2000-12-25
* Token n'est plus un keywordGravatar herbelin2000-12-25
* Effet réorganisation ClassopsGravatar herbelin2000-12-25
* *** empty log message ***Gravatar mayero2000-12-22
* Qualification des inductifs dans Print indGravatar herbelin2000-12-21
* espacementsGravatar herbelin2000-12-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 06:21:08 +0000