aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.ml
Commit message (Expand)AuthorAge
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Indentation + typoGravatar notin2006-09-01
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
* 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
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
* Distinction entre declarations internes (p.ex. _subproof) et declarations uti...Gravatar herbelin2004-03-30
* Memorisation du type de variable (Hyp or Var)Gravatar herbelin2004-03-26
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Petit netoyage dans libGravatar coq2002-12-19
* Petit netoyage des open's et commentairesGravatar coq2002-12-16
* Essai de hconsing local au declarationsGravatar herbelin2002-12-11
* Hash-consing dès la lib_stkGravatar herbelin2002-12-10
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Suppression automatique du corps des définitions locales opaques dansGravatar herbelin2002-08-17
* 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
* Déplacement/renommage de Class.stre_max en Declare.strength_minGravatar herbelin2002-04-16
* Interdiction de nommer une constante comme une variable de section (plus simp...Gravatar herbelin2002-04-12
* - 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
* compat ocaml 3.03Gravatar filliatr2001-12-13
* 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
* 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
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* 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