aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2016-05-27 14:02:39 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-06-29 11:52:52 +0200
commitd4cdb7e41844e1bb77bac9a7b9df423364b996e2 (patch)
tree082d76f16f315acd7f5ef4d153dcd5960f05837a /engine/evd.ml
parent25ffe7f97a907d3508848c81c3e8dcc89559aadd (diff)
Univs: add source locations of levels
For better error messages. The API change is backwards compatible, using a new optional argument.
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index b883db615..1276c5994 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -252,6 +252,7 @@ let instantiate_evar_array info c args =
| _ -> replace_vars inst c
type evar_universe_context = UState.t
+
type 'a in_evar_universe_context = 'a * evar_universe_context
let empty_evar_universe_context = UState.empty