aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r--vernac/obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 624edeffe..1e7721f8f 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -472,7 +472,7 @@ let subst_body expand prg =
let declare_definition prg =
let body, typ = subst_body true prg in
- let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
+ let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
(UState.subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in