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

11 files changed, 26 insertions, 26 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2d65d3ed..392a2cd84 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -47,9 +47,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list }
 
 (** {6 Constants (Definition/Axiom) } *)
+type const_entry_body = constr
 
 type definition_entry = {
-  const_entry_body   : constr;
+  const_entry_body   : const_entry_body;
   const_entry_secctx : Context.section_context option;
   const_entry_type        : types option;
   const_entry_opaque      : bool;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 851803621..62e2d46a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -245,8 +245,8 @@ let safe_push_named (id,_,_ as d) env =
     with Not_found -> () in
   Environ.push_named d env
 
-let push_named_def (id,b,topt) senv =
-  let (c,typ,cst) = Term_typing.translate_local_def senv.env (b,topt) in
+let push_named_def (id,de) senv =
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
   let senv' = add_constraints cst senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46dac02aa..31bb8143e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,7 +34,7 @@ val push_named_assum :
   Id.t * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  Id.t * constr * types option -> safe_environment ->
+  Id.t * definition_entry -> safe_environment ->
     Univ.constraints * safe_environment
 
 (** Adding global axioms or definitions *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83d1ce16c..33a4b55e8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -42,9 +42,9 @@ let local_constrain_type env j cst1 = function
       assert (eq_constr t tj.utj_val);
       t, union_constraints (union_constraints cst1 cst2) cst3
 
-let translate_local_def env (b,topt) =
-  let (j,cst) = infer env b in
-  let (typ,cst) = local_constrain_type env j cst topt in
+let translate_local_def env de =
+  let (j,cst) = infer env de.const_entry_body in
+  let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
     (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index cc6025dab..c9bff84fc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -13,7 +13,7 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> constr * types option ->
+val translate_local_def : env -> definition_entry ->
   constr * types * constraints
 
 val translate_local_assum : env -> types -> types * constraints
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 [];
diff --git a/library/declare.mli b/library/declare.mli
index 602cd64fa..a9cd8f720 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 6ca5bfb83..531526846 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
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index c6f04027b..4d26c4f53 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -148,14 +148,10 @@ let get_locality = function
 | Global -> false
 
 let save with_clean id const (locality,kind) hook =
-  let {const_entry_body = pft;
-       const_entry_secctx = _;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
         let k = Kindops.logical_kind_of_goal_kind kind in
-	let c = SectionLocalDef (pft, tpo, opacity) in
+	let c = SectionLocalDef const in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Discharge | Local | Global ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index aba8a5a81..67bc387ab 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,7 +139,7 @@ let declare_definition ident (local, k) ce imps hook =
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
-    let c = SectionLocalDef(ce.const_entry_body, ce.const_entry_type, false) in
+    let c = SectionLocalDef ce in
     let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
     let () = definition_message ident in
     let () = if Pfedit.refining () then
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 1d953806d..695426d56 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -161,13 +161,10 @@ let look_for_possibly_mutual_statements = function
 
 let save id const do_guard (locality,kind) hook =
   let const = adjust_guardness_conditions const do_guard in
-  let {const_entry_body = pft;
-       const_entry_type = tpo;
-       const_entry_opaque = opacity } = const in
   let k = Kindops.logical_kind_of_goal_kind kind in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
-	let c = SectionLocalDef (pft, tpo, opacity) in
+	let c = SectionLocalDef const in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Local | Global | Discharge ->
@@ -223,7 +220,13 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
         | _ -> anomaly (Pp.str "Not a proof by induction") in
       match locality with
       | Discharge ->
-	  let c = SectionLocalDef (body_i, Some t_i, opaq) in
+          let const = { const_entry_body = body_i;
+              const_entry_secctx = None;
+              const_entry_type = Some t_i;
+              const_entry_opaque = opaq;
+              const_entry_inline_code = false
+          } in
+	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
       | Local | Global ->