aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/uGraph.ml
Commit message (Expand)AuthorAge
* Define and use UGraph.enforce_leq_alg for subtyping inferenceGravatar Gaëtan Gilbert2018-06-22
* Fix restrict_universe_contextGravatar Gaëtan Gilbert2018-05-30
* Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\
* | Always print explanation for univ inconsistency, rm Flags.univ_printGravatar Gaëtan Gilbert2018-04-26
| * universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
|/
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Fix #6878: univ undefined for [with Definition] bad instance size.Gravatar Gaëtan Gilbert2018-03-01
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Replacing costly merges in UGraph.Gravatar Pierre-Marie Pédrot2017-04-18
* Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Universes algorithm : clarified commentsGravatar Jacques-Henri Jourdan2016-01-17
* Fix typos.Gravatar Guillaume Melquiond2016-01-01
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
* New algorithm for universe cycle detections.Gravatar Jacques-Henri Jourdan2015-12-01
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
* Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 10:16:33 +0000