aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
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
2002-01-18Plusieurs arguments autorisés pour Require et Read Moduleherbelin
2001-12-21Bug affichage '++' au lieu de ';'herbelin
2001-12-19Modif précédente trop violente (cf test-suite/success/CasesDep.v)herbelin
2001-12-18On ne peut plus appliquer des arguments à une syntaxe primitiveherbelin
2001-12-18affichage correct du type des inductifs et constructeurs en presencebarras
2001-12-18parsing des branches de Cases au niveau lconstr (au lieu de constr)barras
2001-12-16Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...herbelin
2001-12-13MAJ de la traduction en ast des variables de section en qualidherbelin
2001-12-13compat ocaml 3.03filliatr
2001-12-10- condition de garde (suite)barras
2001-11-29nouvel algo de conversion plus uniformebarras
2001-11-23Retablissement de la commande Existential que j'avais supprime par erreur.clrenard
2001-11-20types vs constrherbelin
2001-11-19Diverses petites simplications de la machine de preuves.clrenard
2001-11-19Re-installation de l'affichage des globaux par des noms courtsherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-08Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]bherbelin
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-11-05GROS COMMIT:barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:14:34 +0000