aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
Commit message (Expand)AuthorAge
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* fixing r11433 again:Gravatar barras2008-10-07
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
* Suppression argument pattern_source du case_info (code jamais utilisé)Gravatar herbelin2007-03-15
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Ajout allowed_sortsGravatar herbelin2006-10-01
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* oubli de code de debuggingGravatar herbelin2006-02-07
* Fonctions retournant les arits des constructeurs et inductifs (suite)Gravatar herbelin2006-01-30
* Fonctions retournant les arits des constructeurs et inductifsGravatar herbelin2006-01-30
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Moving subst_inductive from tacinterp to inductiveops for better for reuse in...Gravatar herbelin2005-02-18
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* Bug control_only_guardGravatar herbelin2004-12-29
* CommentaireGravatar herbelin2004-12-06
* Prise en compte expansion du prédicat du 'match' vis à vis de la dépendanc...Gravatar herbelin2004-08-24
* Nouvelle en-têteGravatar herbelin2004-07-16
* 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