diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/obligations.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index fc1df9f00d..8f637aa325 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -833,6 +833,13 @@ let rec solve_obligation prg num tac = in 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' + in let res = try update_obls {prg with prg_body = prg.prg_body; |