aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Ajout map_inductive_type et map_ind_familyGravatar herbelin2002-06-13
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* Ajout make_arity_signatureGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* GROS COMMIT:Gravatar barras2001-11-05