aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2012-03-01Univ: a better Constraint.compareletouzey
2012-02-29Univ: a faster is_leq test used when possibleletouzey
2012-02-27Univ: correct compare_neq (fix #2703)letouzey
2011-10-26When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyletouzey
2011-10-10Hash-consing of mutual_inductive_body (and Univ.constraints)letouzey
2011-10-02Hash-consing of constr could share moreletouzey
2011-09-22Hash-consing: attempt to stop hash-consing separately constr in declare.mlletouzey
2011-09-08More twicks on hash-consingletouzey
2011-09-07Fix the hconsing of universesletouzey
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-01-25Rewrite sort_universes to minimize the number of universesglondu
2011-01-11In univ.ml, put universe_level primitives in its their own sub-moduleglondu
2011-01-11Add "Print Sorted Universes"glondu
2011-01-11More coherent comment orderingglondu
2010-12-18Univ: try to avoid a few lookup in the universe graphletouzey
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-12-18Revert last commit 13723 on Univ : minor gains and more complex codeletouzey
2010-12-17Univ: an attempt to lazily compact chains of Equiv in a functionnal wayletouzey
2010-12-16Univ: two improvements (speed + space)letouzey
2010-11-03In Univ, unify order_request and constraint_typeglondu
2010-11-02More generic Univ.dump_universesglondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:21:40 +0000