From 1eaebf4ab7616b2be16b957736e80f1d6100eae0 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 9 May 2013 20:48:29 +0000
Subject: 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
---
 toplevel/command.ml |  2 +-
 toplevel/lemmas.ml  | 13 ++++++++-----
 2 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index aba8a5a81c..67bc387abe 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 1d953806dc..695426d56a 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 ->
-- 
cgit v1.2.3