diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index a2e443e5f7..18e7796caf 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 @@ -456,7 +457,7 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity let impls = implicits_of_context params in List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls in - let binder_name = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in + let binder_name = Namegen.next_ident_away (snd id) (Termops.vars_of_env (Global.env())) in let impl, projs = match fields with | [LocalAssum (Name proj_name, field) | LocalDef (Name proj_name, _, field)] when def -> |