aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-09Nettoyage coercions et classesherbelin
2001-11-08Choucroute entre les tables de synchronisation, les options -silent et les et...letouzey
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-11-05Oopsbarras
2001-11-05GROS COMMIT:barras
2001-10-30Reorganisation de Goption. Passage des options l'utilisant en synchroneletouzey
2001-10-26Vérification précoce qu'un lemme n'existe pas déjàherbelin
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-17Amélioration mise en page Print ML Module et Print ML Moduleherbelin
2001-10-16Nettoyage Recordobj et conséquencesherbelin
2001-10-15Orthographeherbelin
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...herbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-09-26Compatibilite Windozherbelin
2001-09-26Le fichier .vo etait ecrit dans un mauvais repertoire si ce dernier etait tro...herbelin
2001-09-24Commentaires pour make docherbelin
2001-09-21Réparation des options Set Printing and coherbelin
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
2001-09-21Protection contre Not_foundherbelin
2001-09-20Correction bug affichage Infix/Distfixherbelin
2001-09-20Transparentbarras
2001-09-20On ignore les répertoires qui ne correspondent pas à des identsherbelin
2001-09-19Protection hd d'une liste videherbelin
2001-09-19make install dans coq_makefile et repertoire associe user-contrib ajoute au l...filliatr
2001-09-19Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...herbelin
2001-09-18Mise en place de noms contenant la section pour Fact et Remarkherbelin
2001-09-18Ajout d'une option et d'une fonction compile pour fabriquer les .voherbelin
2001-09-18Suppression du message d'erreur si une coercion mettant en jeu des locaux n'e...herbelin
2001-09-18Bug discharge d'une déclaration de coercion pour une constante non définie ...herbelin
2001-09-17Blindage de Show Introletouzey
2001-09-14Transformation de Remark/Fact en constantes non visibles sans qualificationherbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables de...herbelin
2001-09-07Suppression des library roots, on teste si un nom est absolu autrementherbelin
2001-09-06Bug default module name (2eme)herbelin
2001-08-10Parsingherbelin
2001-07-10anomaly -> errorclrenard
2001-07-05Débogage discharge des coercions; nettoyageherbelin
2001-07-04ajout Show Intro(s)letouzey
2001-05-29Retablissement de minicoqcoq
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-28Pretty -> Prettypfilliatr
2001-05-28option -qualityfilliatr
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-11application patch Claudiofilliatr
2001-05-03Changement de la structure des points fixesbarras
2001-04-25ligne vide lors de l'affichage des messages d'erreur a toplevel entrebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 04:02:05 +0000