aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
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 b883db615e..1276c5994e 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