aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
AgeCommit message (Expand)Author
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Univ: Use loc even if there are more unbound levelsMatthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:33:27 +0000