aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
AgeCommit message (Expand)Author
2002-12-13correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...letouzey
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-06-13Ajout map_inductive_type et map_ind_familyherbelin
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
2002-02-07petit nettoyage de kernel/inductivebarras
2001-11-20Ajout make_arity_signatureherbelin
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras