aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.mli
Commit message (Expand)AuthorAge
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* DISCLAIMERGravatar puech2009-01-17
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Changement des named_contextGravatar gregoire2005-12-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* 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
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Petit netoyage des open's et commentairesGravatar coq2002-12-16
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* 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
* Raffinement library_partGravatar herbelin2002-02-12
* Ajout library_partGravatar herbelin2002-02-12
* 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
* GROS COMMIT:Gravatar barras2001-11-05
* 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
* Nettoyage des commentairesGravatar herbelin2001-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
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Légère modification lookup_eliminatorGravatar herbelin2001-09-09
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09
* ParsingGravatar herbelin2001-08-10
* Ajout make_elimination_identGravatar herbelin2001-08-01
* Correction d'un commentaire erroné.Gravatar clrenard2001-05-16
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01