aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-26Bug aboutherbelin
2003-09-26Syntaxe plus liberale pour le type des arguments de filtrage du 'match'herbelin
2003-09-26Ajout 'About'herbelin
2003-09-26Re-possibilite changement chaine infixe en passant v7 a v8herbelin
2003-09-24Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-23Utilisation de noms dans 'Implicit Arguments [...]'herbelin
2003-09-23Changement de l'afficheur pour que les variables liées aient un nom indépen...herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-22Distfix aussi adopte le nouveau schema de V8onlyherbelin
2003-09-21Renommages divers.herbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-21Parsing au niveau lconstr des patterns de 'match context'herbelin
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-09-19Mise en place des V8Notation et V8Infix pour déclarer des notations enherbelin
2003-09-18Ajout r gle d'affichage tactiques èéfinies par Notationherbelin
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
2003-09-16En attendant l'afficheur...herbelin
2003-09-12Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et c...herbelin
2003-09-12Fusion des g_*syntaxnew.ml avec les g_*syntax.ml avec sélection dynamique selonherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
2003-09-12MAJ module requis pour le parsing des numérauxherbelin
2003-09-12Affichage des scopes d'argumentsherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'; 'Delimits' -> 'Delimit'herbelin
2003-09-10Passage des projections au niveau 1herbelin
2003-09-109 est associatif a gaucheherbelin
2003-09-10Traduction de Distfixherbelin
2003-09-09Ajout construction If primitive dans constr_expr et rawconstrherbelin
2003-09-09'Grammar tactic' devient 'Tactic Notation'herbelin
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
2003-09-09Code mortherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des r...herbelin
2003-09-06Paramétrisation vis à vis de existential_keyherbelin
2003-09-06'Implicits qid' -> 'Implicit Arguments qid'herbelin
2003-09-06Adapter l'entree de grammaire a la version 7 ou 8herbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Passage de lconstr à constr pour les arguments immédiat de commandesherbelin
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
2003-09-05Impression sans ',' des constructeurs de meme type, pour v8herbelin
2003-09-02Relachement conflit 'with' dans le cas des Module with Definitionherbelin
2003-08-31'Assumptions' sur le modèle général des lieursherbelin
2003-08-31Affichage des inductifs en v8herbelin
2003-08-14Pb de mot-cleherbelin
2003-08-14Ajout token '!' pour correctnessherbelin
2003-08-14Enregistrement tuple_constrherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 02:52:53 +0000