From 2db70092d63065be8a5902764e0d1d5f1ea01e6c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 20 Nov 2017 18:43:31 +0100 Subject: 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. --- vernac/obligations.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'vernac/obligations.ml') 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 -- cgit v1.2.3