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/term_typing.ml | |
| parent | c20eb3a73c4868533bb50555d1979f5b9d821256 (diff) | |
Remove the unused opaque_entry_inline_code field from opaque entries.
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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; } |