aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
Commit message (Expand)AuthorAge
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Fast path when checking equality of universe levels in UState.Gravatar Pierre-Marie Pédrot2017-04-27
| * Code cleaning in unification algorithm for universes.Gravatar Pierre-Marie Pédrot2017-04-27
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Univ: Use loc even if there are more unbound levelsGravatar Matthieu Sozeau2016-06-29
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
* More invariants in UState.Gravatar Pierre-Marie Pédrot2015-11-26
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 05:08:25 +0000