aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-16Prise en compte noms longs dans Implicitsherbelin
2001-02-14Erreur sur commitherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-02-13export a function that is needed in pcoq.bertot
2001-02-13Make sure the initial state used in a protected loop is the state chose exactlybertot
2001-02-12Theoreme opaquesmohring
2001-02-10All errors were not well reported before. In particular syntax errors werebertot
2001-02-09Two pairs of parentheses were missing.bertot
2001-02-09option -m (utilisation memoire)filliatr
2001-02-09exported several functions that are used in the graphical interface pcoq.bertot
2001-02-09changed the design to have command groups executed in a protected mannerbertot
2001-02-08Scratch par defaut si rien n'est specifier dans Add LoadPathherbelin
2001-02-08Suppression warning no .coqrcherbelin
2001-02-08export a function that can be used to retrieve the context correspondingbertot
2001-02-07Meilleure approche du conflit path/freeze/library_root en séquentialisant la...herbelin
2001-02-07Reparation du pretty-print pour les tactiquesdelahaye
2001-02-07Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-06Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-01-31Bug lié au dischargeherbelin
2001-01-31Ajout option Set/Unset/Test Printing Coercionsherbelin
2001-01-31Ajout d'espace dans les règles d'affichage des infix si des lettres figurent...herbelin
2001-01-30Branchement sur Objdefherbelin
2001-01-30Les Objdef introduisent une convertibilité avec les projections dans le test...herbelin
2001-01-30backtrack sur le lexeur de la V6filliatr
2001-01-29pas de warning avec Opaque quand is_silentfilliatr
2001-01-27make docherbelin
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...herbelin
2001-01-24Réorganisation suite ajout de constantes locales dans les Recordsherbelin
2001-01-24Ajout de constantes locales dans les Recordsherbelin
2001-01-18Bug Identity Coercionherbelin
2001-01-09Meta Definition + Tactic Definitiondelahaye
2001-01-05Arite cachee de Match Context + Meta Definitiondelahaye
2001-01-03Let doit etre utilise dans le mode de preuvedelahaye
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-27Bug installation non localeherbelin
2000-12-25Bug discharge process_classherbelin
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; réorg...herbelin
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert afi...herbelin
2000-12-19correction de bugs sur commit précédentherbelin
2000-12-19Découpage des différentes fonctionnalités de build_mutual et definition_st...herbelin
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
2000-12-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
2000-12-15 - suppression mind_extract_paramsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 17:33:48 +0000