aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
AgeCommit message (Expand)Author
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