aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-12-31majfilliatr
2003-12-30option -strict-implicit pas reconnuebarras
2003-12-30ameliorations coqidecoq
2003-12-30majfilliatr
2003-12-29majfilliatr
2003-12-28MAJ 8.0herbelin
2003-12-27Protection contre l'echec des tests parser pour la distribherbelin
2003-12-27Suppression en v8herbelin
2003-12-27MAJherbelin
2003-12-27Type le 'return' comme un typeherbelin
2003-12-27majfilliatr
2003-12-26majfilliatr
2003-12-25majfilliatr
2003-12-24BUGherbelin
2003-12-24*** empty log message ***barras
2003-12-24Parenthesage du terme pour accepter 'of' comme non identherbelin
2003-12-24*** empty log message ***barras
2003-12-24*** empty log message ***barras
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:15:38 +0000