aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declarations.ml
Commit message (Expand)AuthorAge
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* 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
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Documentation mutual_inductive_bodyGravatar herbelin2006-03-18
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* 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
* Ajout recarg_lengthGravatar herbelin2003-11-18
* coupage en deux du bloc pas si mutuellement recursif des module_body & co (.....Gravatar letouzey2003-04-16
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* suppression du champ mind_singl inutilisé dans mutual_inductive_bodyGravatar letouzey2002-12-04
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* GROS COMMIT:Gravatar barras2001-11-05
* 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
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Les params d'inductif deviennent en même temps propre à chaque inductif d'u...Gravatar herbelin2000-12-14
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Ajout mind_arities_envGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Précalcul de la forme canonique des constructeurs et arités pour traiter le...Gravatar herbelin2000-07-01
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeursGravatar herbelin2000-05-31
* Changement nom module Constant en DeclarationsGravatar herbelin2000-05-22