aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* Ajout mis_constructor_nargs_envGravatar herbelin2003-11-18
* Mise en place possibilité de définitions locales dans les paramètres des i...Gravatar herbelin2003-09-06
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Simplification case_infoGravatar herbelin2003-06-10
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* correction (temporaire ?) d'un probleme de Printer.prterm_env utilisant quand...Gravatar letouzey2002-12-13
* 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