diff options
| author | coq | 2002-12-19 16:57:45 +0000 |
|---|---|---|
| committer | coq | 2002-12-19 16:57:45 +0000 |
| commit | bb6f20a2ee88f264fa2c73c5a3ed306008791f7d (patch) | |
| tree | e065248fcc1818fbb7c2f1c29131977c14722a55 /toplevel/command.ml | |
| parent | 57cd43543edfc8961038e2da734c6477ff5ae2bc (diff) | |
Petit netoyage dans lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) |