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 c0acdaf57..5a1c260b1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -362,7 +362,7 @@ let get_body obl =
match obl.obl_body with
| None -> None
| Some (DefinedObl c) ->
- let u = Environ.constant_instance (Global.env ()) c in
+ let u = Univ.AUContext.instance (Environ.constant_context (Global.env ()) c) in
let pc = (c, u) in
Some (DefinedObl pc)
| Some (TermObl c) ->