diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index a2e443e5f..4fb607dec 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -95,8 +95,8 @@ let binders_of_decls = List.map binder_of_decl let typecheck_params_and_fields finite def id pl t ps nots fs = let env0 = Global.env () in - let ctx = Evd.make_evar_universe_context env0 pl in - let evars = ref (Evd.from_ctx ctx) in + let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in + let evars = ref evd in let _ = let error bk (loc, name) = match bk, name with @@ -165,9 +165,10 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let newps = List.map (EConstr.to_rel_decl evars) newps in let typ = EConstr.to_constr evars typ in let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in + let univs = Evd.check_univ_decl evars decl in List.iter (iter_constr ce) (List.rev newps); List.iter (iter_constr ce) (List.rev newfs); - Evd.universe_context ?names:pl evars, typ, template, imps, newps, impls, newfs + univs, typ, template, imps, newps, impls, newfs let degenerate_decl decl = let id = match RelDecl.get_name decl with |