aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/subtyping.ml
Commit message (Expand)AuthorAge
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 07:35:48 +0000