diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 3c0977784d..e8682c1b58 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -623,7 +623,7 @@ let declare_obligation prg obl body ty uctx = let body = prg.prg_reduce body in let ty = Option.map prg.prg_reduce ty in match obl.obl_status with - | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) } + | Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } | Evar_kinds.Define opaque -> let opaque = if get_proofs_transparency () then false else opaque in let poly = pi2 prg.prg_kind in @@ -647,7 +647,7 @@ let declare_obligation prg obl body ty uctx = in if not opaque then add_hint false prg constant; definition_message obl.obl_name; - { obl with obl_body = + true, { obl with obl_body = if poly then Some (DefinedObl constant) else @@ -815,9 +815,9 @@ let obligation_hook prg obl num auto ctx' _ gr = let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in let ctx' = if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' + (* The universe context was declared globally, we continue + from the new global environment. *) + Evd.evar_universe_context (Evd.from_env (Global.env ())) else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -889,8 +889,13 @@ and solve_obligation_by_tac prg obls i tac = (pi2 !prg.prg_kind) !prg.prg_ctx in let uctx = Evd.evar_context_universe_context ctx in - prg := {!prg with prg_ctx = ctx}; - obls.(i) <- declare_obligation !prg obl t ty uctx; + let () = prg := {!prg with prg_ctx = ctx} in + let def, obl' = declare_obligation !prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 !prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + prg := {!prg with prg_ctx = ctx'}); true else false with e when Errors.noncritical e -> |