From 2d9630171c6e17e85eb9c1b51a59fa381716380a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 25 Apr 2018 16:08:51 +0200 Subject: Fix an anomaly when calling Obligation 0 or Obligation -1. I didn't change the parser which expects an integer instead of a positive number because changing it would also mean having worse error messages because of our current LL parser. The error message would have been: Syntax error: 'Tactic' ':=' expected after 'Obligation' (in [vernac:command]). --- vernac/obligations.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index ae1065ef5..1885fc38e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -958,7 +958,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 -- cgit v1.2.3