aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/ind_tables.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/ind_tables.ml')
-rw-r--r--toplevel/ind_tables.ml22
1 files changed, 11 insertions, 11 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index e03c3e9b5..7cf60b7ff 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -123,18 +123,18 @@ let compute_name internal id =
let define internal id c =
let fd = declare_constant ~internal in
let id = compute_name internal id in
- let kn = fd id
- (DefinitionEntry
- { const_entry_body = c;
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false;
- const_entry_inline_code = false
- },
- Decl_kinds.IsDefinition Scheme) in
- (match internal with
+ let entry = {
+ const_entry_body = c;
+ const_entry_secctx = None;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_inline_code = false
+ } in
+ let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+ let () = match internal with
| KernelSilent -> ()
- | _-> definition_message id);
+ | _-> definition_message id
+ in
kn
let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =