index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
subtyping.ml
Commit message (
Expand
)
Author
Age
...
*
Correction bug #1302
herbelin
2007-01-17
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Clarification des contraintes sur le contexte de paramètres des
herbelin
2006-10-17
*
Protection raise en début de séquence (en attendant que le code caché trou...
herbelin
2006-10-12
*
Nouvelle implantation du polymorphisme de sorte pour les familles inductives
herbelin
2006-05-23
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Types inductifs parametriques
mohring
2005-11-02
*
1. added code to handle the inclusion of inductive types and constructors in
sacerdot
2005-01-17
*
HUGE COMMIT
sacerdot
2005-01-03
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-12-09
*
suppression du champ mind_singl inutilisé dans mutual_inductive_body
letouzey
2002-12-04
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
Comparaisons des types pendant le sous-typage reactive
coq
2002-09-30
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Petites corrections ici et la
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
[prev]