diff options
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1ab24b670..1f401b4e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -480,10 +480,9 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let env = Global.env () in let uvars = Univ.LSet.union - (Univops.universes_of_constr env typ) - (Univops.universes_of_constr env body) in + (Univops.universes_of_constr typ) + (Univops.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in @@ -865,7 +864,7 @@ let obligation_terminator name num guard hook auto pf = else UState.union prg.prg_ctx ctx in let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (_, obl) = declare_obligation prg obl body ty uctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in let prg_ctx = @@ -874,10 +873,12 @@ let obligation_terminator name num guard hook auto pf = polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx else - (** The first obligation declares the univs of the constant, + (** The first obligation, if defined, + declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) - UState.make (Global.universes ()) + if defined then UState.make (Global.universes ()) + else ctx in let prg = { prg with prg_ctx } in try |