aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/discharge.ml
Commit message (Expand)AuthorAge
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Types inductifs parametriquesGravatar mohring2005-11-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREGravatar herbelin2004-11-19
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* 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