From bbec0ea51b4dfef1ddb09a2f876323aa1547f643 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 08:14:28 +0200
Subject: Dedicated type for opaque entries in the kernel.

Even more invariants can be enforced this way.
---
 tactics/declare.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 2178a7c54c..d4fdff76bf 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -175,12 +175,12 @@ let cast_proof_entry e =
 let cast_opaque_proof_entry e =
   let open Proof_global in
   {
-    const_entry_body = e.proof_entry_body;
-    const_entry_secctx = e.proof_entry_secctx;
-    const_entry_feedback = e.proof_entry_feedback;
-    const_entry_type = e.proof_entry_type;
-    const_entry_universes = e.proof_entry_universes;
-    const_entry_inline_code = e.proof_entry_inline_code;
+    opaque_entry_body = e.proof_entry_body;
+    opaque_entry_secctx = e.proof_entry_secctx;
+    opaque_entry_feedback = e.proof_entry_feedback;
+    opaque_entry_type = e.proof_entry_type;
+    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