aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/subtyping.ml
Commit message (Collapse)AuthorAge
* Corrections de gestion des univers et modules + meilleure gestions des ↵Gravatar coq2002-12-09
| | | | | | noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression du champ mind_singl inutilisé dans mutual_inductive_bodyGravatar letouzey2002-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy manuelles dans le codeGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy experimentale temporaire...Gravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comparaisons des types pendant le sous-typage reactiveGravatar coq2002-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3052 85f007b7-540e-0410-9357-904b9bb8a0f7
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petites corrections ici et laGravatar coq2002-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7