aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
AgeCommit message (Collapse)Author
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
Now it is a private field, locations are optional.
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
Suggested by @ppedrot
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Pierre Letouzey
module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-06-29Univ: Use loc even if there are more unbound levelsMatthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
For better error messages. The API change is backwards compatible, using a new optional argument.
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
longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l).
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
This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar.