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 44f20a088..e59482b71 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 = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in + let univs = Evd.universe_context ~names:[] ~extensible:true sigma in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry (definition_entry ~types:typ_f ~poly ~univs |