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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel/command.ml')

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
-- 
cgit v1.2.3