diff options
| author | Hugo Herbelin | 2020-11-22 11:28:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-22 11:28:06 +0100 |
| commit | f5ccc82ce8f2db919b288f3a853dbf238615de59 (patch) | |
| tree | fc2151e909aac796f7ddc0ebdd4b6b0029a527d0 | |
| parent | 9c841105fe2b51305abcba7bd8a574705dbd1adf (diff) | |
Fixes another instance of bug #7967: restriction of universes in "Context".
| -rw-r--r-- | test-suite/bugs/closed/bug_7967.v | 4 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 5 |
2 files changed, 6 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_7967.v b/test-suite/bugs/closed/bug_7967.v index 2c8855fd54..987a820831 100644 --- a/test-suite/bugs/closed/bug_7967.v +++ b/test-suite/bugs/closed/bug_7967.v @@ -1,2 +1,6 @@ Set Universe Polymorphism. Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. + +(* A similar bug *) +Context (C := ltac:(let y := constr:(Type) in exact nat)). +Check C@{}. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 9e850ff1c7..f8f2193e03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -257,9 +257,10 @@ let context ~poly l = let sigma = Evd.from_env env in let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false env sigma l in (* Note, we must use the normalized evar from now on! *) - let sigma = Evd.minimize_universes sigma in let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in + let sigma, ctx = Evarutil.finalize ~abort_on_undefined_evars:false + sigma (fun nf -> List.map (RelDecl.map_constr_het nf) ctx) in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> let {binder_name=name}, b, t = RelDecl.to_tuple d in @@ -267,8 +268,6 @@ let context ~poly l = | Anonymous -> user_err Pp.(str "Anonymous variables not allowed in contexts.") | Name id -> id in - let b = Option.map (EConstr.to_constr sigma) b in - let t = EConstr.to_constr sigma t in let impl = let open Glob_term in let search x = match x.CAst.v with | Some (Name id',max) when Id.equal name id' -> |