aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typing.ml')
-rw-r--r--pretyping/typing.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f34f7efe..7702355b8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c =
let j = execute env evdref c in
(* side-effect on evdref *)
if refresh then
- Evarsolve.refresh_universes false !evdref j.uj_type
+ Evarsolve.refresh_universes false env !evdref j.uj_type
else !evdref, j.uj_type
let solve_evars env evdref c =