aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2001-06-222 bugs: typevarlist pour inductifs + args pour flexiblesletouzey
2001-06-20Ajout d'un Setoid_rewrite et meilleure resolution des petits sous-buts géné...clrenard
2001-06-20Normalisation du predicat synthetise pour les Caseclrenard
2001-06-20oubli de Elimdep dans le Makefilebarras
2001-06-19Un bug corrige.clrenard
2001-06-19Ajouts des theories du paradoxe de Berardidelahaye
2001-06-19Extension des parametres de Clear + Instdelahaye
2001-06-19Extension des parametres de Cleardelahaye
2001-06-19Oubli Save + je sais plusmayero
2001-06-18Ajouts de lemmes (pour Float)mayero
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
2001-06-18Interpretation MetaId + Progress + Instdelahaye
2001-06-16code mortherbelin
2001-06-15Fix d'un bug de Tautodelahaye
2001-06-13plus besoin de separer les ?barras
2001-06-13Prise en compte env local (et defs locales) dans Changeherbelin
2001-06-12Ajout d'une normalisation (beta_iota) pour les predicats de Cases inferes aut...clrenard
2001-06-12Ajout des entrees puor Setoid_replace.clrenard
2001-06-12Ajout de la tactique Setoid_replace.clrenard
2001-06-11Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Caseclrenard
2001-06-11Fix de quelques bugs syntaxiques de Ltacdelahaye
2001-06-05Ajout de deux anciens bugsdelahaye
2001-06-04Correction bug outsidemayero
2001-06-01Correction d'un bug du a un Intros trop violentdelahaye
2001-06-01Backtrack vers comportement de la V6 pour eviter les globaux dans le nommage ...herbelin
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...herbelin
2001-05-31Amelioration - subjective - de l'affichage des Hintherbelin
2001-05-29Retablissement de minicoqcoq
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-29Chgt de MAKE= ...letouzey
2001-05-29Correction d'un bug du pretty-printclrenard
2001-05-28option -bytefilliatr
2001-05-28Pretty -> Prettypfilliatr
2001-05-28option -qualityfilliatr
2001-05-28patch Claudiofilliatr
2001-05-28nettoyagefilliatr
2001-05-25Oups: flingait les Dglob dans optimizeletouzey
2001-05-25erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un Letletouzey
2001-05-25Remplacement push_rec_types (Rel) pour Fix parpush_named_rec_typesherbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-22majletouzey
2001-05-22suite du musée des horreursletouzey
2001-05-22ordre des inductifs + axiome-typeletouzey
2001-05-18Erreur dans un commentaire ...clrenard
2001-05-18Modification afin de permettre plusieurs modifs successives d'une commandeclrenard
2001-05-16Correction d'un commentaire erroné.clrenard
2001-05-15Ajout d'une fonction de remplacement d'un sous-terme par un terme.clrenard
2001-05-15Modification pour passage p-automatesmohring
2001-05-15Correction bug predicat du Cases (suite)herbelin
2001-05-14mise en place extraction haskellfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 09:05:32 +0000