From 5de7daa41e677798e4169a3e6350af0df12017e8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 09:32:25 +0200
Subject: Remove the unused opaque_entry_inline_code field from opaque entries.

---
 kernel/term_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.ml')

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;
       }
 
-- 
cgit v1.2.3