aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
AgeCommit message (Expand)Author
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
2001-11-05GROS COMMIT:barras
2001-09-20Nettoyage des commentairesherbelin
2001-09-09Passage aux univers algébriquesherbelin
2001-07-03Ajout hashconsing universherbelin
2001-05-29Facilites pour le debogguage des univers.coq
2001-03-28amelioration de la structure des universbarras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-28Prise en compte du repertoire dans le section path; utilisation de dirpath po...herbelin
2000-10-06MAJ pr_uniherbelin
2000-10-06correction bug univers (dummy_univ)filliatr
1999-09-25ensembles de contraintes d'universfilliatr
1999-09-03modules Libobject et Summary (partiel)filliatr
1999-08-30un petit effort de presentation dans les interfacesfilliatr
1999-08-26 - abstractionfilliatr
1999-08-24mach et himsg; typage sans extractionfilliatr
1999-08-20machine: execute = typage avec universfilliatr
1999-08-18module Reduction (fin)filliatr
1999-08-18module Reduction (debut)filliatr
1999-08-17generic, term et evdfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:28:08 +0000