aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08Some dead code removal + cleanupsletouzey
2008-11-16Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)letouzey
2008-11-15Correct display of constraints for Print Universes "dumpfile"letouzey
2008-11-14Faster comparison of universesletouzey
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
2008-03-15Application de refresh_universes dans typing.ml et retyping.ml : lesherbelin
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module 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-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
2006-03-29Inductifs avec polymorphisme de sorte (version initiale)herbelin
2005-09-08Simplification message d'anomalieherbelin
2005-05-05Bug affichage graphe universherbelin
2005-05-05MAJ commentaires et inversion du sens du graphe de contraintes pour extensibi...herbelin
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-10-20bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)barras
2004-07-16Nouvelle en-têteherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-12-13compat ocaml 3.03filliatr
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:59:44 +0000