aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.mli
Commit message (Expand)AuthorAge
* 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
* 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
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05