diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index f925a2d07..da6624032 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -225,7 +225,7 @@ let build_id_coercion idf_opt source poly = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(Evd.universe_context sigma) + (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in |