aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-12-24Ajout delimiteur et arguments de scope pour listherbelin
2003-12-24Bug affichage Decomposeherbelin
2003-12-24MAJ Notationherbelin
2003-12-24La correction precedente a mis en evidence un defaut de l'utilisation de intr...herbelin
2003-12-24changement de pose en set (pose n'etait pas utilise avec la semantiquebarras
2003-12-24majfilliatr
2003-12-23'of' restait par erreur mot-cle dans psyntax.ml4 en v8herbelin
2003-12-23Reparation semantique casse de Pose en v7herbelin
2003-12-23Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...herbelin
2003-12-23Retablissement de GIntuition juste pour FSetsherbelin
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
2003-12-23*** empty log message ***barras
2003-12-23Affichage opaqueherbelin
2003-12-23Bug commit precedentherbelin
2003-12-23Renommages des hypotheses transformees car en raison des possibles dependance...herbelin
2003-12-23Changement numero magique; message d'erreur en cas de mauvaise syntaxeherbelin
2003-12-23majfilliatr
2003-12-22Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...herbelin
2003-12-22MAJherbelin
2003-12-22majfilliatr
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
2003-12-21Traduction PolyList/List dans la qualificationherbelin
2003-12-20MAJ messages d'erreurs en accord avec la docherbelin
2003-12-20Bug rattrapage erreur locate_referenceherbelin
2003-12-20MAJherbelin
2003-12-20majfilliatr
2003-12-20majfilliatr
2003-12-19Suppression de l'espace avant les notations commencant par un identherbelin
2003-12-19Inductive Types : seuls les petits types sont unitairesmohring
2003-12-19Bug affichage des metas dans un environnement avec definitions locales (bug 277)herbelin
2003-12-19Substitution dans REvar; reparation bug 277herbelin
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application po...herbelin
2003-12-19Reset Initial uniquement interactivementherbelin
2003-12-19name_app accessible a tous dans Nameopsherbelin
2003-12-19majfilliatr
2003-12-18majfilliatr
2003-12-17Prise en compte des sous-termes imbriqués pour 'simpl ident at nums'herbelin
2003-12-17ajout test de non-regression Clear d'une def localebarras
2003-12-17majfilliatr
2003-12-16Correction bug 371 (sub_match retournait des instances non closes)herbelin
2003-12-16MAJ suppression 250herbelin
2003-12-16coqide menus on golasmarche
2003-12-16exists | --> exists ,barras
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
2003-12-16bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)barras
2003-12-16majfilliatr
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-15'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoinherbelin
2003-12-15Protection du nom Eval pour eviter conflit avec Eval inherbelin
2003-12-15majfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 23:22:41 +0000