aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.mli
AgeCommit message (Expand)Author
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-03diverses modifs pour ocamlwebfilliatr
2000-04-20Abstraction du type typed_type (un pas vers les jugements 2 niveaux)herbelin
2000-03-21Modification de type_of_case, type_case_branches, etcherbelin
2000-03-21Prise en compte nouveau case_info dans type_caseherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-11Intégration initiale du Casesherbelin
1999-12-09Discharge (encore bugge)filliatr
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-12-07correction bug construct_referencefilliatr
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-12-01poursuite de Vernacentriesfilliatr
1999-12-01 - environment -> safe_environmentfilliatr
1999-11-25Backtrack sur modif Evd.evd_conclherbelin
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-10-20 - documentation repertoire proofs/filliatr
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
1999-10-14module Logicfilliatr
1999-10-08deplacements des var. ex. hors du noyaufilliatr
1999-09-25ensembles de contraintes d'universfilliatr
1999-09-07 - minicoq : definition inductifs; syntaxe a->bfilliatr
1999-08-26environnement surfilliatr
1999-08-26mach -> typing; machops -> typeopsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:46:46 +0000