diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c71feb52b..89b18d254 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -888,7 +888,7 @@ in let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in Univ.Instance.empty, Evd.evar_universe_context ctx' else - let (_, uctx) = UState.universe_context ctx' in + let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in |