aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
Commit message (Expand)AuthorAge
* (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
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Nettoyage de GenericGravatar herbelin2000-05-31
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en int...Gravatar herbelin2000-03-28
* Prise en compte nouveau case_info dans type_caseGravatar herbelin2000-03-21
* Ajout de RecordGravatar herbelin2000-01-11
* - global_reference traite des variablesGravatar filliatr1999-12-03
* Version initialeGravatar herbelin1999-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 23:17:04 +0000