diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2017-11-20 18:43:31 +0100 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2017-11-22 11:14:46 +0100 |
| commit | 2db70092d63065be8a5902764e0d1d5f1ea01e6c (patch) | |
| tree | 478c124734b6444141378a1df22488f77b2102c7 /vernac/obligations.ml | |
| parent | 2a857da2a88855a6c9f0fa7e48a8700c1613e0c7 (diff) | |
Fix universe polymorphic Program obligations.
The universes of the obligations should all be non-algebraic as they
might appear in instances of other obligations and instances only take
non-algebraic universes as arguments.
Diffstat (limited to 'vernac/obligations.ml')
| -rw-r--r-- | vernac/obligations.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml index ed4d8b888..a44de66e9 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -678,6 +678,7 @@ let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind obl_deps = d; obl_tac = tac }) obls, b in + let ctx = UState.make_flexible_nonalgebraic ctx in { prg_name = n ; prg_body = b; prg_type = reduce t; prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); @@ -841,6 +842,9 @@ let obligation_terminator name num guard hook auto pf = Inductiveops.control_only_guard (Global.env ()) body; (** Declare the obligation ourselves and drop the hook *) let prg = get_info (ProgMap.find name !from_prg) in + (** Ensure universes are substituted properly in body and type *) + let body = EConstr.to_constr sigma (EConstr.of_constr body) in + let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in let ctx = Evd.evar_universe_context sigma in let prg = { prg with prg_ctx = ctx } in let obls, rem = prg.prg_obligations in |