aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2003-11-29Renommages discrets dans RIneq et Znumtheoryherbelin
2003-11-27Suite commit precedentherbelin
2003-11-27Qualification des noms utilisateurs en cas de collision avec un nom nouveauherbelin
2003-11-26Traduction de @; simplification traduction des identherbelin
2003-11-25modif lexer: ident peut commencer par _barras
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les composantes...herbelin
2003-11-21ajout Pnat et Pcompare_antisymherbelin
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans...herbelin
2003-11-18reparation bug moins unaire (erreur de PP)barras
2003-11-18Mise en place systeme de qualification des noms renommes; Renommages dans Rin...herbelin
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-17Un ident filtre est liant seulement si une variable deja liee (sinon bug dans...herbelin
2003-11-16Bug filtrage pour inversion notationherbelin
2003-11-14Conflit renommageherbelin
2003-11-14Oublis dans les rennomagesherbelin
2003-11-14Suppression renommages dans Peanoherbelin
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...barras
2003-11-12Nouvelle et derniere vague de renommageherbelin
2003-11-12Test de la reference principale plutot que le module dans lequel se trouve la...herbelin
2003-11-09Quelqes renommages lies a Zorderherbelin
2003-11-05Nouvelle vague de renommageherbelin
2003-11-04Extension de zarithherbelin
2003-11-01Extensibilite de la grammaires des patternsherbelin
2003-11-01Renommage Topconstr.map_aconstr_with_binders_locherbelin
2003-11-01Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_locherbelin
2003-11-01Ajout CPatNotation; renommage map_aconstr_with_binders_locherbelin
2003-11-01Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...herbelin
2003-10-30Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ...herbelin
2003-10-28Ajout de Print Visibilityherbelin
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
2003-10-21Optimisation de gen_constant_in_modulesherbelin
2003-10-21Bug Locate Notationherbelin
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
2003-10-16print_projections a true juste pour le bench nocturneherbelin
2003-10-16Message d'erreurherbelin
2003-10-16Debranchement de l'affichage systematique des projections avec la notation po...herbelin
2003-10-16Debranchement de l'affichage systematique des projections avec la notation po...herbelin
2003-10-15Gestion encore plus affinee des implicitesherbelin
2003-10-14Gestion affinee des implicitesherbelin
2003-10-14Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteurherbelin
2003-10-14identityT = identityherbelin
2003-10-14Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...herbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-08Pb residuel avec la prise en compte des parametres implicites d'inductifsherbelin
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ...herbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-10-01cosmetiqueherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:38:19 +0000