diff options
| author | Pierre-Marie Pédrot | 2019-06-20 09:32:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 11:02:11 +0200 |
| commit | 5de7daa41e677798e4169a3e6350af0df12017e8 (patch) | |
| tree | caee657e8bca3b0742ad208a9d5e0a6c23b81350 /kernel | |
| parent | c20eb3a73c4868533bb50555d1979f5b9d821256 (diff) | |
Remove the unused opaque_entry_inline_code field from opaque entries.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 6016510189..f73111d35f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,7 +85,7 @@ type 'a opaque_entry = { opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; opaque_entry_universes : universes_entry; - opaque_entry_inline_code : bool } +} type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6cb7a22a15..a0cc2974d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -695,7 +695,7 @@ let constant_entry_of_side_effect eff = opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; - opaque_entry_inline_code = cb.const_inline_code } + } else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 86d79ba044..eca22869d2 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } @@ -187,7 +187,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } |