diff options
Diffstat (limited to 'vernac/class.ml')
-rw-r--r-- | vernac/class.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/class.ml b/vernac/class.ml index e59482b71..68fd22cb6 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -212,7 +212,7 @@ let build_id_coercion idf_opt source poly = Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) in - let univs = Evd.universe_context ~names:[] ~extensible:true sigma in + let univs = Evd.to_universe_context sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs |