aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
AgeCommit message (Expand)Author
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2015-12-01Remove unneeded fixpoint in normalize_context_set. Note that it is noMatthieu Sozeau
2015-11-26More invariants in UState.Pierre-Marie Pédrot
2015-11-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot