aboutsummaryrefslogtreecommitdiff
path: root/parsing/q_coqast.ml4
AgeCommit message (Expand)Author
2004-01-09bugs avec Pose et Assertbarras
2003-12-01Nouvelle tactique EExistsclrenard
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-18reparation bug moins unaire (erreur de PP)barras
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-09-21Mise en place d'implicites par noms en v8herbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-10Ajout notation c.(f) en v8 pour les projections de Recordherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-07Ajout cas Matchherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-12*** empty log message ***barras
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-11-14Restauration échappement MLherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-07fix forbidden currified constructorsddr
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
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
2001-11-05GROS COMMIT:barras
2001-08-10Pour contourner un bug de camlp4 3.02herbelin
2001-08-10Parsingherbelin
2001-04-04renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...filliatr
2001-03-15entetesfilliatr
2000-11-24Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...herbelin
2000-01-13Nettoyage des fichiers de parsingherbelin
2000-01-07Restructuration printer et parserherbelin
1999-09-08compilation des grammaires (ouf)filliatr
1999-09-08modules grammaire Coqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 01:20:21 +0000