aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-21added the .vo checker (with independent Makefile)barras
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-01-19Prise en compte des univers algébriques dans les types inférés dansherbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2005-05-05Code v7 obsoleteherbelin
2004-07-16Nouvelle en-têteherbelin
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