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.

---
 tactics/declare.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 3840aa6be1..fdb8155038 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -184,7 +184,6 @@ let cast_opaque_proof_entry e =
     opaque_entry_feedback = e.proof_entry_feedback;
     opaque_entry_type = typ;
     opaque_entry_universes = e.proof_entry_universes;
-    opaque_entry_inline_code = e.proof_entry_inline_code;
   }
 
 let get_roles export eff =
-- 
cgit v1.2.3