aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
Commit message (Expand)AuthorAge
* Nettoyage suite nouveaux avertissements Y et Z de ocaml 3.09Gravatar herbelin2005-11-08
* 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
* Suppression StronglyClassical, StronglyConstructive devient plus concretement...Gravatar herbelin2003-11-08
* Set devient predicatif par defautGravatar herbelin2003-10-28
* Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse laGravatar herbelin2002-12-10
* Déplacement du hash-consing vers declare.mlGravatar herbelin2002-12-10
* RenoncementGravatar herbelin2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* petite erreur dans le typage des let-inGravatar barras2002-03-28
* petit nettoyage de kernel/inductiveGravatar barras2002-02-07
* compat ocaml 3.03Gravatar filliatr2001-12-13
* types vs constrGravatar herbelin2001-11-20
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
* Rétablissement de la persistance des Cast; typage des LetIn sans recours à ...Gravatar herbelin2001-11-08
* GROS COMMIT:Gravatar barras2001-11-05
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Bugs de vérification de la bonne fondation en présence de définitions loca...Gravatar herbelin2001-10-03
* Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...Gravatar herbelin2001-09-19
* Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ...Gravatar herbelin2001-09-10
* Remplacement du tableau du nombre d'args utiles pour la réduction des Cases ...Gravatar herbelin2001-07-21
* Depliage des let-in dans le test de gardeGravatar herbelin2001-07-03
* Normalisation du predicat synthetise pour les CaseGravatar clrenard2001-06-20
* erreur DeBruijn causant un RecursionNotOnInductiveType quand le type est un LetGravatar letouzey2001-05-25
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Changement de la structure des points fixesGravatar barras2001-05-03
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* Amélioration message d'erreur conditions de gardeGravatar herbelin2001-03-12
* nouvelle implantation de la reductionGravatar barras2001-03-01
* retire profileGravatar mohring2001-02-28
* Changement de subst_metaGravatar mohring2001-02-28
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Chgt signature de type_of_existentialGravatar herbelin2001-02-07
* MAJ commentairesGravatar herbelin2000-12-14
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* Bug dans la gestion du contexte en présence de Fix dans le calcul de gardeGravatar herbelin2000-11-27
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Prise en compte de l'environnement dans les tests de bonne fondaisonGravatar herbelin2000-10-11
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
* Correction incompatibilites dans la fn des types des inductifsGravatar herbelin2000-10-06
* Renommage AppL en AppGravatar herbelin2000-10-01
* Bug message erreurGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 22:30:48 +0000