aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-07Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...herbelin
2002-11-07fix forbidden currified constructorsddr
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-11-03Ajout delimiteurs dans les motifs de Casesherbelin
2002-10-30Désagglutination du squelette de la notation et de sa précédenceherbelin
2002-10-29Mais laisser la syntaxe (!id) aussi disponible !herbelin
2002-10-29Parenthèse non obligatoires autour de !id sans argumentherbelin
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
2002-10-23Le test de redondance d'une règle était trop fortherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:02:32 +0000