aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/inductive.ml
Commit message (Expand)AuthorAge
* revert on commit r12553Gravatar barras2009-12-07
* two improvements of the guard condition:Gravatar barras2009-12-01
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
* fixing r11433 again:Gravatar barras2008-10-07
* fixed pb with r11433Gravatar barras2008-10-07
* bug #1951: polymorphic indtypes: universe subst was not performed in the type...Gravatar barras2008-10-06
* 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
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* improved the implementation of rtreeGravatar barras2008-03-18
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
* Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)Gravatar herbelin2007-10-04
* cosmetiqueGravatar barras2006-12-12
* bug condition de gardeGravatar barras2006-12-08
* Débranchement du polymorphisme de sorte sur les définitions dans TypeGravatar herbelin2006-10-30
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Correction de 2 bugs critiques du polymorphisme d'universGravatar herbelin2006-10-27
* Correction de deux cas où les types inductifs n'étaient pas comparésGravatar herbelin2006-10-05
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Correction bug du polymorphisme de sort des inductifs (cas où les variables ...Gravatar herbelin2006-06-22
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* correction bugs de condition de garde (fix + cofix)Gravatar barras2006-05-12
* subst. explicites avec vecteursGravatar barras2006-05-09
* fixed bug #804: removed useless reduction in fix guard checkingGravatar barras2006-05-03
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Variable inutiliséeGravatar herbelin2006-01-21
* 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
* parametres inductifsGravatar mohring2005-11-28
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Utilisation de la non-équivalence d'inductifs pour le case_info (cf message ...Gravatar herbelin2005-07-21
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* CommentaireGravatar herbelin2004-12-06
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
* Nouvelle en-têteGravatar herbelin2004-07-16
* Un bug résiduel (mais pas bien méchant) du noyauGravatar herbelin2004-05-27
* message d'erreur de garde des cofixGravatar barras2003-09-22
* bug fix: term reduced in bad envGravatar barras2003-09-18
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* - amelioration des messages d'erreur de la condition de gardeGravatar barras2002-12-18