aboutsummaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
AgeCommit message (Expand)Author
2003-11-18Ajout mis_constructor_nargs_envherbelin
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des i...herbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-06-10Simplification case_infoherbelin
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...letouzey
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