aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.ml
AgeCommit message (Expand)Author
2000-05-22Suite restructuration inductifs; changement nom module Constant en Declarationsherbelin
2000-05-18Restructuration des outils pour les inductifs.herbelin
2000-05-04Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)herbelin
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
2000-03-17Un cast inutileherbelin
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