diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1f1be243e..29d745732 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -858,18 +858,17 @@ let obligation_terminator name num guard hook auto pf = in let obl = { obl with obl_status = false, status } in let uctx = Evd.evar_context_universe_context ctx in - let (def, obl) = declare_obligation prg obl body ty uctx in + let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in try ignore (update_obls prg obls (pred rem)); - if def then - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then + if pred rem > 0 then + begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then ignore (auto (Some name) None deps) - end + end with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) |