aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* Types inductifs parametriquesGravatar mohring2005-11-02
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* compatibility with POWERPCGravatar gregoire2004-11-22
* 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
* 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
* bugs avec Pose et AssertGravatar barras2004-01-09
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* (Re-)branchement sur les noms reserves pour les args d'inductif (dont Record)Gravatar herbelin2003-09-16
* Mise en place possibilité de définitions locales dans les paramètres des r...Gravatar herbelin2003-09-06
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Que des niveaux d'univers frais dans le type des constantes globalesGravatar herbelin2002-09-29
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Intgration uniforme de coercions dans les dclarations (Variable and co) et re...Gravatar herbelin2002-06-03
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* Utilisation des de Bruijn pour la constructions des records et de leur projec...Gravatar herbelin2002-05-13
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* compat ocaml 3.03Gravatar filliatr2001-12-13
* nouvel algo de conversion plus uniformeGravatar barras2001-11-29
* Amélioration messages d'erreur arité incorrecte (notamment record)Gravatar herbelin2001-11-21
* 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
* ParsingGravatar herbelin2001-08-10
* entetesGravatar filliatr2001-03-15
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
* correction de bugs sur commit précédentGravatar herbelin2000-12-19
* Découpage des différentes fonctionnalités de build_mutual et definition_st...Gravatar herbelin2000-12-19
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
* uniformisation messages d'erreurGravatar filliatr2000-11-27
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* 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
* Messages d'erreursGravatar herbelin2000-09-15
* Abstraction de constrGravatar herbelin2000-09-14