From 1f96d480842a1206a9334d0c8b1b6cc4647066ef Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 20 Sep 2001 18:10:57 +0000
Subject: Transparent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 28f26a3af..f75128148 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,7 +21,7 @@ type constant_body = {
   const_type : types;
   const_hyps : section_context;
   const_constraints : constraints;
-  mutable const_opaque : bool }
+  const_opaque : bool }
 
 let is_defined cb = 
   match cb.const_body with Some _ -> true | _ -> false
@@ -31,8 +31,9 @@ let is_opaque cb = cb.const_opaque
 (*s Global and local constant declaration. *)
 
 type constant_entry = {
-  const_entry_body : constr;
-  const_entry_type : constr option }
+  const_entry_body   : constr;
+  const_entry_type   : constr option;
+  const_entry_opaque : bool }
 
 type local_entry =
   | LocalDef of constr
-- 
cgit v1.2.3