index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
uGraph.ml
Age
Commit message (
Expand
)
Author
2018-04-28
Merge PR #6892: Cleanup implementation of normalize_context_set a bit
Pierre-Marie Pédrot
2018-04-26
Always print explanation for univ inconsistency, rm Flags.univ_print
Gaëtan Gilbert
2018-04-13
universe normalisation: put equivalence class partition in UGraph
Gaëtan Gilbert
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-01
Fix #6878: univ undefined for [with Definition] bad instance size.
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-09
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-07-11
Cleaning up the implementation of module subtyping in the kernel.
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-04-18
Replacing costly merges in UGraph.
Pierre-Marie Pédrot
2016-11-30
Fix UGraph.check_eq!
Matthieu Sozeau
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-01-17
Universes algorithm : clarified comments
Jacques-Henri Jourdan
2016-01-01
Fix typos.
Guillaume Melquiond
2015-12-27
Removing dead code.
Pierre-Marie Pédrot
2015-12-01
New algorithm for universe cycle detections.
Jacques-Henri Jourdan
2015-11-26
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
