aboutsummaryrefslogtreecommitdiff
path: root/.depend
AgeCommit message (Expand)Author
2006-03-22Made pretyping a functor over a coercion implementation. Pretyping.Default us...msozeau
2006-03-22- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deherbelin
2006-03-15Ajout de theories/FSets contenant la partie "light" de FSets et FMap:letouzey
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
2006-03-08 r8620@thot: notin | 2006-03-08 11:44:16 +0100notin
2006-03-05majcoq
2006-03-02majcoq
2006-02-27majcoq
2006-02-27dp: sortie Whyfilliatr
2006-02-22majcoq
2006-02-21majcoq
2006-02-20majcoq
2006-02-17majcoq
2006-02-09majcoq
2006-02-08majcoq
2006-02-08Julien:bertot
2006-02-07majcoq
2006-02-04majcoq
2006-02-03majcoq
2006-02-01majcoq
2006-02-01New version of functional induction / inversion. By Julien Forest,coq
2006-01-31majcoq
2006-01-30majcoq
2006-01-28majcoq
2006-01-24majcoq
2006-01-21majcoq
2006-01-16majcoq
2006-01-16dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoletouzey
2006-01-12majcoq
2006-01-11majcoq
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-08majcoq
2006-01-07majcoq
2006-01-04majcoq
2005-12-31majcoq
2005-12-28majcoq
2005-12-27majcoq
2005-12-26majcoq
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-25majcoq
2005-12-21majcoq
2005-12-20majcoq
2005-12-17majcoq
2005-12-02Changement des named_contextgregoire
2005-11-28majcoq
2005-11-18majcoq
2005-11-17majcoq
2005-11-17A la demande de Julien Forestletouzey
2005-11-08majcoq
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:09:48 +0000