aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
Commit message (Expand)AuthorAge
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Tables logarithmiques pour les coercions + nettoyageGravatar herbelin2003-06-08
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* la table PARAMETER n'existe plus (mergé dans la table CONSTANT)Gravatar letouzey2002-12-03
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Renoncement à distinguer les types "constr" et "types"; nettoyageGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* compat ocaml 3.03Gravatar filliatr2001-12-13
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* corrections mineures suite au commit de restructuration du noyauGravatar barras2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* 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
* TransparentGravatar barras2001-09-20
* Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...Gravatar herbelin2001-09-19
* Mise en place de noms contenant la section pour Fact et RemarkGravatar herbelin2001-09-18
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* Débogage discharge des coercions; nettoyageGravatar herbelin2001-07-05
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* bug Reset et SectionsGravatar filliatr2001-02-28
* Stringmap -> IdmapGravatar herbelin2001-02-22
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Restructuration de classops; évolution en une version mieux intégrée au re...Gravatar herbelin2001-02-05
* Branchement sur ObjdefGravatar herbelin2001-01-30
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Bug discharge process_classGravatar herbelin2000-12-25
* PrinterGravatar mohring2000-12-15
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* Prise en compte des définitions localesGravatar herbelin2000-11-27
* sp au lieu de id dans END-SECTIONGravatar herbelin2000-11-26
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* implicites manuelsGravatar filliatr2000-11-21
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* Petit bug entre close_section'sGravatar herbelin2000-11-20
* Tables séparées pour chaque type de global; calcul de la Nametab de la sect...Gravatar herbelin2000-11-20
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
* out_variable (Liboject.obj -> ...) distibgue de get_variableGravatar filliatr2000-11-08
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ...Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06