aboutsummaryrefslogtreecommitdiff
path: root/kernel/univ.ml
AgeCommit message (Expand)Author
2013-10-29Optimizing universes: tail-rec, allocation friendly [compare_leq].ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Specializing hash functions for widely used types.ppedrot
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-04Fix comment for new string syntax (OCaml trunk).xclerc
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-03-05More monomorphization.ppedrot
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-10* Implementing the "union by rank" optimisation in univ.mlpboutill
2012-11-26Small cleaning of interface in Univppedrot
2012-11-22Monomorphization (kernel)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-04-05Shortcuts and optimizations of comparisonsxclerc
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-22Univ: switch the order of int and dir_path in UniverseLevel.Levelletouzey
2012-03-12Univ: avoid recording dummy universe constraints u<=u or u=uletouzey
2012-03-02Noise for nothingpboutill
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 14:26:50 +0000