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

3 files changed, 7 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ca18874d41..4f88a6b0e1 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 [];
diff --git a/library/declare.mli b/library/declare.mli
index 602cd64faf..a9cd8f7205 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -29,7 +29,7 @@ open Nametab
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 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
@@ -59,7 +59,7 @@ val declare_constant :
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> Id.t -> ?types:constr -> constr -> constant
+  ?local:bool -> Id.t -> ?types:constr -> Entries.const_entry_body -> constant
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
diff --git a/library/global.mli b/library/global.mli
index 6ca5bfb83d..531526846c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -37,7 +37,7 @@ val env_is_empty : unit -> bool
 
 (** {6 Extending env with variables and local definitions } *)
 val push_named_assum : (Id.t * types) -> Univ.constraints
-val push_named_def   : (Id.t * constr * types option) -> Univ.constraints
+val push_named_def   : (Id.t * definition_entry) -> Univ.constraints
 
 (** {6 ... } *)
 (** Adding constants, inductives, modules and module types.  All these