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 1a3b1f39b..8843e52f4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -962,7 +962,7 @@ and obligation (user_num, name, typ) tac =
let num = pred user_num in
let prg = get_prog_err name in
let obls, rem = prg.prg_obligations in
- if num < Array.length obls then
+ if num >= 0 && num < Array.length obls then
let obl = obls.(num) in
match obl.obl_body with
None -> solve_obligation prg num tac