Use definition_entry to declare local definitions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ca18874d4..4f88a6b0e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,7 +50,7 @@ let add_cache_hook f = cache_hook := f
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of constr * types option * bool (* opacity *)
+  | SectionLocalDef of definition_entry
   | SectionLocalAssum of types * bool (* Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -67,9 +67,9 @@ let cache_variable ((sp,_),o) =
         let cst = Global.push_named_assum (id,ty) in
 	let impl = if impl then Implicit else Explicit in
 	impl, true, cst
-    | SectionLocalDef (c,t,opaq) ->
-        let cst = Global.push_named_def (id,c,t) in
-        Explicit, opaq, cst in
+    | SectionLocalDef de ->
+        let cst = Global.push_named_def (id,de) in
+        Explicit, de.const_entry_opaque, cst in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl;
   Dischargedhypsmap.set_discharged_hyps sp [];