summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
-rw-r--r--plugins/subtac/subtac_obligations.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 6a5878b3..dfcc8526 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -663,6 +663,7 @@ let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
let admit_obligations n =
let prg = get_prog_err n in
let obls, rem = prg.prg_obligations in
+ let obls = Array.copy obls in
Array.iteri
(fun i x ->
match x.obl_body with