aboutsummaryrefslogtreecommitdiff
path: root/kernel/uGraph.ml
AgeCommit message (Expand)Author
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2021-01-05Move universe printing out of AcyclicGraph.Pierre-Marie Pédrot
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
2020-08-26Fix algebraic comparison with sprop on one sideGaëtan Gilbert
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-27Small API additions to kernel/univGaëtan Gilbert
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2018-12-17Make ugraph implementation abstract wrt universe specificsGaëtan Gilbert
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-16Use universe names when printing to dot.Gaëtan Gilbert
2018-11-16Make UGraph printing independent of hash orderGaëtan Gilbert
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-05-30Fix restrict_universe_contextGaëtan Gilbert
2018-04-28Merge PR #6892: Cleanup implementation of normalize_context_set a bitPierre-Marie Pédrot
2018-04-26Always print explanation for univ inconsistency, rm Flags.univ_printGaëtan Gilbert
2018-04-13universe normalisation: put equivalence class partition in UGraphGaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-01Fix #6878: univ undefined for [with Definition] bad instance size.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-04-18Replacing costly merges in UGraph.Pierre-Marie Pédrot
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-17Universes algorithm : clarified commentsJacques-Henri Jourdan
2016-01-01Fix typos.Guillaume Melquiond
2015-12-27Removing dead code.Pierre-Marie Pédrot
2015-12-01New algorithm for universe cycle detections.Jacques-Henri Jourdan
2015-11-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:20:17 +0000