aboutsummaryrefslogtreecommitdiff
path: root/toplevel/class.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r--toplevel/class.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 8512e00c56..436aa8409c 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -248,7 +248,7 @@ let build_id_coercion idf_opt source =
const_entry_type = Some typ_f;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()} in
- let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+ let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
ConstRef kn
let check_source = function