aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
AgeCommit message (Expand)Author
2000-03-07Redondancesherbelin
2000-01-26Abstraction de l'implémentation des signatures de Sign en vue intégration d...herbelin
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
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-06declarations eliminations / debuggae inductifs (debut)filliatr
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-12-01poursuite de Vernacentriesfilliatr
1999-12-01 - Typing -> Safe_typingfilliatr
1999-11-25Backtrack sur modif Evd.evd_conclherbelin
1999-11-24MAJ pour fusion avec pretypingherbelin
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
1999-10-18 - déplacement (encore une fois !) des variables existentielles : elles sontfilliatr
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-09-07mise en place commandes minicoqfilliatr
1999-09-03 - environnements videsfilliatr
1999-08-27suppression champs inutiles dans constantes et inductifs; verification defini...filliatr
1999-08-26environnement surfilliatr
1999-08-26mach -> typing; machops -> typeopsfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:18:05 +0000