aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre se...herbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-08-10Parsingherbelin
2001-07-03Ajout hashconsing universherbelin
2001-05-29Facilites pour le debogguage des univers.coq
2001-05-03Changement de la structure des points fixesbarras
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-10-06Correction incompatibilites dans la fn des types des inductifsherbelin
2000-10-06correction bug univers (dummy_univ)filliatr
1999-09-25ensembles de contraintes d'universfilliatr
1999-08-26 - abstractionfilliatr