aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declare.mli
Commit message (Expand)AuthorAge
* 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
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Ajout alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* find_section_variable : un traducteur id -> sp pour variables de section; var...Gravatar herbelin2000-12-25
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* NettoyageGravatar herbelin2000-11-26
* Prise en compte de noms absolus dans la nametab + nettoyageGravatar herbelin2000-11-26
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21