From bb6f20a2ee88f264fa2c73c5a3ed306008791f7d Mon Sep 17 00:00:00 2001
From: coq
Date: Thu, 19 Dec 2002 16:57:45 +0000
Subject: Petit netoyage dans lib

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 81ee49bd65..1c636275a4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -106,7 +106,7 @@ let declare_definition ident local bl red_option c typopt =
     error "Evaluation under a local context not supported";
   let ce' = red_constant_entry ce red_option in
   match local with
-    | Local when Lib.is_section_p (Lib.cwd ()) ->
+    | Local when Lib.sections_are_opened () ->
         let c =
           SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
         let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in
@@ -134,7 +134,7 @@ let declare_assumption ident (local,kind) bl c =
   let c = prod_rawconstr c bl in
   let c = interp_type Evd.empty (Global.env()) c in
   match local with
-    | Local when Lib.is_section_p (Lib.cwd ()) ->
+    | Local when Lib.sections_are_opened () ->
         let r = 
           declare_variable ident 
             (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
@@ -500,7 +500,7 @@ let save id const kind hook =
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
   begin match kind with
-    | IsLocal when Lib.is_section_p (Lib.cwd ()) ->
+    | IsLocal when Lib.sections_are_opened () ->
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in
 	hook Local (VarRef id)
-- 
cgit v1.2.3