aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2003-03-21*** empty log message ***barras
2003-03-14reparations suite a la nouvelle syntaxe:barras
2003-03-13Ajout réaffichage SubClassherbelin
2003-03-12*** empty log message ***barras
2003-03-12Renommage indpar pour usage plus generalherbelin
2003-03-04Bug délimiteur de scope en vieil affichage astherbelin
2003-03-03Retour vieil afficheurherbelin
2003-02-27Interpretation des entiers dans les reels via les scopesdesmettr
2003-02-27Nouvelle syntaxe style 'Inductive color : Set := black, blue, white : color'...herbelin
2003-02-27Correction test token normalherbelin
2003-02-27Le lexeur et Notation savent reconnaître si un unicode des blocsherbelin
2003-02-27Retour nouvel afficheurherbelin
2003-02-17Affinement entree annotherbelin
2003-02-13Debugger plus informatifdelahaye
2003-02-05Ajout du traducteurdesmettr
2003-01-31Pour satisfaire ProofGeneralcoq
2003-01-30Adds a possibility to construct a term as if it had been parsed throughbertot
2003-01-27Deux p\'tits trucs ;)coq
2003-01-22I changed the interface to make sure SearchAbout is defined according tobertot
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2003-01-19Rétablissement pr_patternherbelin
2003-01-16Bugs affichageherbelin
2003-01-15Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...herbelin
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
2003-01-09Export M + Module M <: SIGcoq
2003-01-07Retour printer ast pour V7.4herbelin
2003-01-06SearchAboutfilliatr
2002-12-28Prise en compte notations dans les extensions de motiffherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-21Affinement affichageherbelin
2002-12-21Plus de notation cablees dans 'annot'herbelin
2002-12-19Petit netoyage dans libcoq
2002-12-19bug: Global.env() executé au chargement -> eta-expansionletouzey
2002-12-15Meilleure factorisation des entrées NEXT internesherbelin
2002-12-15Quelques bugs d'affichage; mise en place du nouveau printer de vieille syntaxeherbelin
2002-12-15Pas de 0 dans positiveherbelin
2002-12-13possibilité de faire Print M avec M module ou modtype au lieu de Print Modul...letouzey
2002-12-12Ajout du vernac Proof withgregoire
2002-12-10Bugs diversherbelin
2002-12-10Ajout options -v7 et -v8, et commandes V7only et V8onlyherbelin
2002-12-09Problèmes et améliorations affichage; Changement Simplherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-12-04Correction divers bugs d'affichage; explicitation du niveau de grammaire quan...herbelin
2002-12-04Modification Require Frommohring
2002-12-03la table PARAMETER n'existe plus (mergé dans la table CONSTANT)letouzey
2002-12-03bug de non-indépendance des règles d'affichage et parsing vis à vis du nom...herbelin
2002-12-03bugs d'affichage (confusion key/scope dans les délimiteurs)herbelin
2002-12-03Calcul de l'associativité même pour les Grammar avec plusieurs clausesherbelin
2002-12-03Le '.' peut faire partie d'un tokenherbelin
2002-12-02Remplacement de Syntactic Definition par Notationherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 22:06:56 +0000