diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
| commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
| tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /plugins/subtac/subtac_obligations.ml | |
| parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) | |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 1 |
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 |