aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Expand)AuthorAge
* Fixing critical inductive polymorphism bug found by Bruno.Gravatar herbelin2011-10-05
* Indtypes: remove useless and wrong generic equality test on constr arrayGravatar puech2011-07-29
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* fixed (serious) bug #2353: non-recursive parameters of nested inductive types...Gravatar barras2010-07-16
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* fixed bug #2224 (Error message in positivity check fixed)Gravatar vsiles2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixing bug #2156 (non positive occurrence error message displayed "Rel"'s).Gravatar herbelin2009-12-30
* 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
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* fixed minor environment issues when checking inductive typesGravatar barras2008-09-02
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* 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
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...Gravatar barras2008-03-18
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
* bug in infos_and_sort: type of constructor was not reduced enoughGravatar barras2007-11-07
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
* Suppresion de la catégorie des inductifs singletons larges dontGravatar herbelin2007-02-09
* Correction du bug #1273 (problème avec les paramètres non récursivement un...Gravatar notin2006-12-12
* 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
* - 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 trou de typage des éliminations d'inductifs introduit dans commit...Gravatar herbelin2006-05-13
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
* Bug calcul consnrealargs + bug calcul occurrences non positives + modifs cosm...Gravatar herbelin2006-03-18
* *** empty log message ***Gravatar barras2006-01-20
* Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...Gravatar herbelin2006-01-10
* Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...Gravatar herbelin2005-12-17
* 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
* Suppression code inactif et commentaire apparemment incorrect (pour éviter c...Gravatar herbelin2005-09-09
* Correction bug #983Gravatar herbelin2005-06-28
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* correspondance des records et noms de champs de records entre un module et sa...Gravatar letouzey2004-06-25
* Inductive Types : seuls les petits types sont unitairesGravatar mohring2003-12-19
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25