diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:35:36 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:35:36 +0200 |
| commit | f1050affbd0009ea12794bd193184c80f938e1e6 (patch) | |
| tree | b8a7a957c3fe89643543a7ea23fe7a539a1c50c7 /vernac/obligations.ml | |
| parent | 82dc05efc11514c2c05ec17e448e0b4b322e7c86 (diff) | |
| parent | 2d9630171c6e17e85eb9c1b51a59fa381716380a (diff) | |
Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.
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 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 |