aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-12réparation de la protection contre les clauses indiscernables de TACTIC EXTE...herbelin
2002-10-12Notation 2:Check et 2:Evalherbelin
2002-10-12Restriction sur la forme des Syntactic Definition et re-localisation en fonct...herbelin
2002-10-07Lazy manuelles dans le codecoq
2002-10-05Lazy experimentale temporaire...coq
2002-10-05pretty s'appellait prettyp mais il est revenu sous son ancien nomherbelin
2002-09-27passage a ocaml 3.06herbelin
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-30Réparation d'un bug qui considérait les composantes d'un QUALIDherbelin
2002-07-15Pb de factorisation camlp4herbelin
2002-07-15Pour assurer une compatibilite avec la 7.3herbelin
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
2002-06-19Coercion de la syntaxe des motifs non atomiquesherbelin
2002-06-13Petits beug d'affichages.gregoire
2002-06-05Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotificationherbelin
2002-06-05Fusion entre la nouvelle et l'ancienne syntaxe de HintDestructherbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et re...herbelin
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Implante la macro camlp4 VERNAC COMMAND EXTENDherbelin
2002-05-29Implante la macro camlp4 TACTIC EXTENDherbelin
2002-05-27Ajout de Eval, Inst et Checkdelahaye
2002-05-15Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage deherbelin
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-16Typoherbelin
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-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-03-29Correction bug infix sur des varaiablesmohring
2002-03-19Ajout de l'entrée ne_constrarg_listdelahaye
2002-03-17Meilleure gestion de la reduction dans Fielddelahaye
2002-02-14option -dump-glob pour coqdocfilliatr
2002-02-11substitution et pattern modulo letbarras
2002-02-07petit nettoyage de kernel/inductivebarras
2002-02-01Ajout tactiques Rename et Pose; modifications pour Inversionherbelin
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 18:12:32 +0000