aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* suppression de pop_namedGravatar barras2002-02-22
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Raffinement library_partGravatar herbelin2002-02-12
* Ajout library_partGravatar herbelin2002-02-12
* Correction de l'ordre des open (sachant que de toutes façons, unGravatar herbelin2002-01-24
* Pas d'assert false dans un try with !Gravatar herbelin2002-01-18
* Plusieurs arguments autorisés pour Require et Read Module; mise en place d'u...Gravatar herbelin2002-01-18
* Suppression de la dépendance des .vo en le nom physique des modulesGravatar herbelin2002-01-07
* MAJ nombre magiqueGravatar herbelin2001-12-19
* probleme des Require dans les sectionsGravatar barras2001-12-17
* compat ocaml 3.03Gravatar filliatr2001-12-13
* - condition de garde (suite)Gravatar barras2001-12-10
* Rustine pour garder la compatibilité avec la 7.1 pour l'ordre des imports sa...Gravatar herbelin2001-12-05
* reparation de LocateGravatar barras2001-11-29
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Mise en place d'une méthode directe pour indiquer le type des déclarations ...Gravatar herbelin2001-11-19
* Re-installation de l'affichage des globaux par des noms courtsGravatar herbelin2001-11-19
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Déplacement et export de type_of_global dans GlobalGravatar herbelin2001-11-09
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Reorganisation de Goption. Passage des options l'utilisant en synchroneGravatar letouzey2001-10-30
* Patch de goption.ml pour faire marcher les options synchrones. Passage des op...Gravatar letouzey2001-10-24
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...Gravatar herbelin2001-10-12
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* One more boolean test bugGravatar herbelin2001-09-24
* Bug test booléenGravatar herbelin2001-09-24
* Réparation des options Set Printing and coGravatar herbelin2001-09-21
* Protection contre des arguments farfelus pour les implicites manuelsGravatar herbelin2001-09-21
* make docGravatar filliatr2001-09-21
* TransparentGravatar barras2001-09-20
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Nettoyage des commentairesGravatar herbelin2001-09-20
* Nombre magique pour la V7.1Gravatar herbelin2001-09-20
* Pas de warning pour le -I . par défaut de CoqGravatar herbelin2001-09-20
* warning silencieuxGravatar filliatr2001-09-20
* Restriction de l'avertissement add_loadpath au mode verbeuxGravatar herbelin2001-09-20
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Autorisation de surcharge d'un -R par un -IGravatar herbelin2001-09-19
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...Gravatar herbelin2001-09-19
* TypoGravatar herbelin2001-09-19
* Tentative de canonisation des répertoires physiquesGravatar herbelin2001-09-18
* Mise en place de noms contenant la section pour Fact et RemarkGravatar herbelin2001-09-18
* Quelques heuristiques pour gérer des représentations similaires de paths sy...Gravatar herbelin2001-09-18
* Transformation de Remark/Fact en constantes non visibles sans qualificationGravatar herbelin2001-09-14
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10