aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.mli
Commit message (Expand)AuthorAge
* 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
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
* ensembles de contraintes d'universGravatar filliatr1999-09-25
* - minicoq : definition inductifs; syntaxe a->bGravatar filliatr1999-09-07
* environnement surGravatar filliatr1999-08-26
* mach -> typing; machops -> typeopsGravatar filliatr1999-08-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-01 04:51:51 +0000