aboutsummaryrefslogtreecommitdiff
path: root/parsing/astterm.ml
AgeCommit message (Expand)Author
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-14Utilisation d'une construction spéciale SECVAR pour gérer laherbelin
2002-05-10Plus de souplesse pour les constructeurs encapsulés sous des définitionsherbelin
2002-04-18Suppression d'un warning plus surprenant qu'utileherbelin
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
2002-04-10Syntactic Definition autorisée dans les motifs de Cases (utile notammentherbelin
2002-02-14option -dump-glob pour coqdocfilliatr
2001-12-13compat ocaml 3.03filliatr
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-10-15Nouvelle correction du bug confusion entre implicites de locaux et de globauxherbelin
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-10-11Bug collision entre les implicites d'un global et les variables locales de mÃ...herbelin
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
2001-10-02Ajout de dynamiques pour les quotations constr et tacticdelahaye
2001-09-21Mise en place globalisation optionnelle pour Infix/Distfixherbelin
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...herbelin
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...herbelin
2001-09-09Préparation à la mise en place d'univers algébriquesherbelin
2001-08-10Parsingherbelin
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-05-29Facilites pour le debogguage des univers.coq
2001-04-25message d'erreur pour rattrapper l'anomalie avec SQUASHbarras
2001-04-24Messages d'erreur Casesherbelin
2001-03-15entetesfilliatr
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en compte...herbelin
2001-02-08Simplificationsherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au re...herbelin
2001-01-31Bug localisation des Syntactif Definitionherbelin
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
2001-01-19Autour des quotations avec Casesherbelin
2000-12-20Suppression warning variable de filtrage en majusculeherbelin
2000-12-14Amélioration message d'erreurherbelin
2000-12-14Bug dans les alias de Casesherbelin
2000-11-24Réorganisation autour de globalize_constrherbelin
2000-11-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...herbelin
2000-11-21Prise en compte des implicites dans les regles de grammairesherbelin
2000-11-20Acceptation des noms qualifiés; utilisation de global_reference dans pattern...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:45:04 +0000