aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.mli
Commit message (Expand)AuthorAge
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Compatibilité du polymorphisme de constantes avec les sections.Gravatar herbelin2006-10-29
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* changement des _sym par _comm dans setoid_ringGravatar bgregoir2006-10-27
* Déplacement de on_judgment_type de Typeops vers TermopsGravatar herbelin2006-10-06
* - Indtypes: en attente opinion CoRN, les occurrences de Type non explicitesGravatar herbelin2006-05-28
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
* Changement des named_contextGravatar gregoire2005-12-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* 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
* 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
* 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
* Chgt signature de type_of_existentialGravatar herbelin2001-02-07
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Relative prend sigma en plus pour la normalisation du message d'erreurGravatar herbelin2000-06-29
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
* Nettoyage de GenericGravatar herbelin2000-05-31
* Restructuration des outils pour les inductifs.Gravatar herbelin2000-05-18
* diverses modifs pour ocamlwebGravatar filliatr2000-05-03
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
* Modification de type_of_case, type_case_branches, etcGravatar herbelin2000-03-21
* Prise en compte nouveau case_info dans type_caseGravatar herbelin2000-03-21
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* Intégration initiale du CasesGravatar herbelin1999-12-11
* Discharge (encore bugge)Gravatar filliatr1999-12-09
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* correction bug construct_referenceGravatar filliatr1999-12-07
* Intégration du Termast et du Retyping de HH, et modifications connexesGravatar herbelin1999-12-01
* poursuite de VernacentriesGravatar filliatr1999-12-01
* - environment -> safe_environmentGravatar filliatr1999-12-01
* Backtrack sur modif Evd.evd_conclGravatar herbelin1999-11-25
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* - documentation repertoire proofs/Gravatar filliatr1999-10-20
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
* module LogicGravatar filliatr1999-10-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 06:50:36 +0000