aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Expand)AuthorAge
* A version of Univ.check_eq with no anomaly for Evd.set_eq_sortGravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* * Implementing the "union by rank" optimisation in univ.mlGravatar pboutill2012-12-10
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Univ: switch the order of int and dir_path in UniverseLevel.LevelGravatar letouzey2012-03-22
* Univ: avoid recording dummy universe constraints u<=u or u=uGravatar letouzey2012-03-12
* Noise for nothingGravatar pboutill2012-03-02
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
* Univ: a better Constraint.compareGravatar letouzey2012-03-01
* Univ: a faster is_leq test used when possibleGravatar letouzey2012-02-29
* Univ: correct compare_neq (fix #2703)Gravatar letouzey2012-02-27
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Hash-consing of mutual_inductive_body (and Univ.constraints)Gravatar letouzey2011-10-10
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
* More twicks on hash-consingGravatar letouzey2011-09-08
* Fix the hconsing of universesGravatar letouzey2011-09-07
* Tentative to make unification check types at every instanciation of anGravatar msozeau2011-03-11
* Rewrite sort_universes to minimize the number of universesGravatar glondu2011-01-25
* In univ.ml, put universe_level primitives in its their own sub-moduleGravatar glondu2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* More coherent comment orderingGravatar glondu2011-01-11
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
* Univ: two improvements (speed + space)Gravatar letouzey2010-12-16
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
* More generic Univ.dump_universesGravatar glondu2010-11-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12