diff options
| author | Matthieu Sozeau | 2014-07-10 15:40:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-10 15:40:41 +0200 |
| commit | 6663052ccd613faf4282bd73121a44398bd3ba76 (patch) | |
| tree | 82d2aa5239e9a2110fb8de763f45fad98241d899 /toplevel | |
| parent | a071ac178ee9e6ca0cbae14db24e10775b0af881 (diff) | |
Better handling of the universe context in case of Admitted proof obligations.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/obligations.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 8f637aa325..13f9e9339d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -834,11 +834,16 @@ let rec solve_obligation prg num tac = let obls = Array.copy obls in let _ = obls.(num) <- obl in let ctx' = - if not (pi2 prg.prg_kind) (* Not polymorphic *) then - (* This context is already declared globally, we cannot - instantiate the rigid variables anymore *) - Evd.abstract_undefined_variables ctx' - else ctx' + let ctx = + match ctx' with + | None -> prg.prg_ctx + | Some ctx' -> ctx' + in + if not (pi2 prg.prg_kind) (* Not polymorphic *) then + (* This context is already declared globally, we cannot + instantiate the rigid variables anymore *) + Evd.abstract_undefined_variables ctx + else ctx in let res = try update_obls |