aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/subtyping.ml
Commit message (Expand)AuthorAge
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* cf. 12945Gravatar soubiran2010-04-16
* Patch on subtyping check of opaque constants.Gravatar soubiran2010-01-06
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...Gravatar soubiran2008-06-18
* Ajout d'un comportement special du sous-typage pour les constantes opaques.Gravatar soubiran2008-06-09
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* correction bug 1839Gravatar soubiran2008-04-25
* correction bug 1839Gravatar soubiran2008-04-22
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* Petite correction sur un message d'erreur renvoyé au sous typage.Gravatar soubiran2007-01-30
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Prise en compte des univers algébriques dans les types inférés dansGravatar herbelin2007-01-19
* Correction bug #1302Gravatar herbelin2007-01-17
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Clarification des contraintes sur le contexte de paramètres desGravatar herbelin2006-10-17
* Protection raise en début de séquence (en attendant que le code caché trou...Gravatar herbelin2006-10-12
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* 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
* 1. added code to handle the inclusion of inductive types and constructors inGravatar sacerdot2005-01-17
* HUGE COMMITGravatar sacerdot2005-01-03
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* 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
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* suppression du champ mind_singl inutilisé dans mutual_inductive_bodyGravatar letouzey2002-12-04
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* Comparaisons des types pendant le sous-typage reactiveGravatar coq2002-09-30
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Petites corrections ici et laGravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02