aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-com.tex6
-rw-r--r--doc/refman/RefMan-ext.tex2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--library/lib.ml84
-rw-r--r--toplevel/coqtop.ml8
-rw-r--r--toplevel/usage.ml1
6 files changed, 50 insertions, 53 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index bef0a1686..45230fb6e 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -123,12 +123,6 @@ The following command-line options are recognized by the commands {\tt
valid for {\tt coqc} as the toplevel module name is inferred from the
name of the output file.
-\item[{\tt -notop}]\ %
-
- Use the empty logical path for the toplevel module name instead of {\tt
- Top}. Not valid for {\tt coqc} as the toplevel module name is
- inferred from the name of the output file.
-
\item[{\tt -exclude-dir} {\em directory}]\ %
Exclude any subdirectory named {\em directory} while
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b475a5233..1d423f8b1 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -991,7 +991,7 @@ but library file names based on other roots can be obtained by using
{\Coq} commands ({\tt coqc}, {\tt coqtop}, {\tt coqdep}, \dots) options
{\tt -Q} or {\tt -R} (see Section~\ref{coqoptions}). Also, when an
interactive {\Coq} session starts, a library of root {\tt Top} is
-started, unless option {\tt -top} or {\tt -notop} is set (see
+started, unless option {\tt -top} is set (see
Section~\ref{coqoptions}).
\subsection{Qualified names
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e4b3fcbf1..2312f891c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -71,7 +71,7 @@ module NamedDecl = Context.Named.Declaration
- [env] : the underlying environment (cf Environ)
- [modpath] : the current module name
- [modvariant] :
- * NONE before coqtop initialization (or when -notop is used)
+ * NONE before coqtop initialization
* LIBRARY at toplevel of a compilation or a regular coqtop session
* STRUCT (params,oldsenv) : inside a local module, with
module parameters [params] and earlier environment [oldsenv]
diff --git a/library/lib.ml b/library/lib.ml
index 4fd29a94d..ddd2ed6af 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -97,21 +97,30 @@ let segment_of_objects prefix =
let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
-let lib_stk = ref ([] : library_segment)
+type lib_state = {
+ comp_name : Names.DirPath.t option;
+ lib_stk : library_segment;
+ path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t);
+}
-let comp_name = ref None
+let initial_lib_state = {
+ comp_name = None;
+ lib_stk = [];
+ path_prefix = initial_prefix;
+}
+
+let lib_state = ref initial_lib_state
let library_dp () =
- match !comp_name with Some m -> m | None -> default_library
+ match !lib_state.comp_name with Some m -> m | None -> default_library
(* [path_prefix] is a pair of absolute dirpath and a pair of current
module path and relative section path *)
-let path_prefix = ref initial_prefix
-let cwd () = fst !path_prefix
-let current_prefix () = snd !path_prefix
-let current_mp () = fst (snd !path_prefix)
-let current_sections () = snd (snd !path_prefix)
+let cwd () = fst !lib_state.path_prefix
+let current_prefix () = snd !lib_state.path_prefix
+let current_mp () = fst (snd !lib_state.path_prefix)
+let current_sections () = snd (snd !lib_state.path_prefix)
let sections_depth () = List.length (Names.DirPath.repr (current_sections ()))
let sections_are_opened () = not (Names.DirPath.is_empty (current_sections ()))
@@ -132,7 +141,7 @@ let make_kn id =
let mp,dir = current_prefix () in
Names.make_kn mp dir (Names.Label.of_id id)
-let make_oname id = Libnames.make_oname !path_prefix id
+let make_oname id = Libnames.make_oname !lib_state.path_prefix id
let recalc_path_prefix () =
let rec recalc = function
@@ -142,18 +151,18 @@ let recalc_path_prefix () =
| _::l -> recalc l
| [] -> initial_prefix
in
- path_prefix := recalc !lib_stk
+ lib_state := { !lib_state with path_prefix = recalc !lib_state.lib_stk }
let pop_path_prefix () =
- let dir,(mp,sec) = !path_prefix in
- path_prefix := pop_dirpath dir, (mp, pop_dirpath sec)
+ let dir,(mp,sec) = !lib_state.path_prefix in
+ lib_state := { !lib_state with path_prefix = pop_dirpath dir, (mp, pop_dirpath sec)}
let find_entry_p p =
let rec find = function
| [] -> raise Not_found
| ent::l -> if p ent then ent else find l
in
- find !lib_stk
+ find !lib_state.lib_stk
let split_lib_gen test =
let rec collect after equal = function
@@ -174,7 +183,7 @@ let split_lib_gen test =
| _ -> findeq (hd::after) before)
| [] -> None
in
- match findeq [] !lib_stk with
+ match findeq [] !lib_state.lib_stk with
| None -> error "no such entry"
| Some r -> r
@@ -199,10 +208,10 @@ let split_lib_at_opening sp =
(* Adding operations. *)
let add_entry sp node =
- lib_stk := (sp,node) :: !lib_stk
+ lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk }
let pull_to_head oname =
- lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk
+ lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk }
let anonymous_id =
let n = ref 0 in
@@ -277,7 +286,7 @@ let start_mod is_type export id mp fs =
if exists then
user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix} ;
prefix
let start_module = start_mod false
@@ -299,16 +308,16 @@ let end_mod is_type =
with Not_found -> error "No opened modules."
in
let (after,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
+ lib_state := { !lib_state with lib_stk = before };
add_entry oname (ClosedModule (List.rev (mark::after)));
- let prefix = !path_prefix in
+ let prefix = !lib_state.path_prefix in
recalc_path_prefix ();
(oname, prefix, fs, after)
let end_module () = end_mod false
let end_modtype () = end_mod true
-let contents () = !lib_stk
+let contents () = !lib_state.lib_stk
let contents_after sp = let (after,_,_) = split_lib sp in after
@@ -316,14 +325,14 @@ let contents_after sp = let (after,_,_) = split_lib sp in after
(* TODO: use check_for_module ? *)
let start_compilation s mp =
- if !comp_name != None then
+ if !lib_state.comp_name != None then
error "compilation unit is already started";
if not (Names.DirPath.is_empty (current_sections ())) then
error "some sections are already opened";
let prefix = s, (mp, Names.DirPath.empty) in
let () = add_anonymous_entry (CompilingLibrary prefix) in
- comp_name := Some s;
- path_prefix := prefix
+ lib_state := { !lib_state with comp_name = Some s;
+ path_prefix = prefix }
let end_compilation_checks dir =
let _ =
@@ -344,7 +353,7 @@ let end_compilation_checks dir =
with Not_found -> anomaly (Pp.str "No module declared")
in
let _ =
- match !comp_name with
+ match !lib_state.comp_name with
| None -> anomaly (Pp.str "There should be a module name...")
| Some m ->
if not (Names.DirPath.equal m dir) then anomaly
@@ -355,8 +364,8 @@ let end_compilation_checks dir =
let end_compilation oname =
let (after,mark,before) = split_lib_at_opening oname in
- comp_name := None;
- !path_prefix,after
+ lib_state := { !lib_state with comp_name = None };
+ !lib_state.path_prefix,after
(* Returns true if we are inside an opened module or module type *)
@@ -514,7 +523,7 @@ let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
let open_section id =
- let olddir,(mp,oldsec) = !path_prefix in
+ let olddir,(mp,oldsec) = !lib_state.path_prefix in
let dir = add_dirpath_suffix olddir id in
let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
if Nametab.exists_section dir then
@@ -523,7 +532,7 @@ let open_section id =
add_entry (make_oname id) (OpenedSection (prefix, fs));
(*Pushed for the lifetime of the section: removed by unfrozing the summary*)
Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
- path_prefix := prefix;
+ lib_state := { !lib_state with path_prefix = prefix };
if !Flags.xml_export then Hook.get f_xml_open_section id;
add_section ()
@@ -549,8 +558,8 @@ let close_section () =
error "No opened section."
in
let (secdecls,mark,before) = split_lib_at_opening oname in
- lib_stk := before;
- let full_olddir = fst !path_prefix in
+ lib_state := { !lib_state with lib_stk = before };
+ let full_olddir = fst !lib_state.path_prefix in
pop_path_prefix ();
add_entry oname (ClosedSection (List.rev (mark::secdecls)));
if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
@@ -561,7 +570,7 @@ let close_section () =
(* State and initialization. *)
-type frozen = Names.DirPath.t option * library_segment
+type frozen = lib_state
let freeze ~marshallable =
match marshallable with
@@ -578,18 +587,15 @@ let freeze ~marshallable =
Some(n,OpenedSection(op,Summary.empty_frozen))
| n, ClosedSection _ -> Some (n,ClosedSection [])
| _, FrozenState _ -> None)
- !lib_stk in
- !comp_name, lib_stk
+ !lib_state.lib_stk in
+ { !lib_state with lib_stk }
| _ ->
- !comp_name, !lib_stk
+ !lib_state
-let unfreeze (mn,stk) =
- comp_name := mn;
- lib_stk := stk;
- recalc_path_prefix ()
+let unfreeze st = lib_state := st
let init () =
- unfreeze (None,[]);
+ unfreeze initial_lib_state;
Summary.init_summaries ();
add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c4d8dfec9..0cd5498fe 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -134,11 +134,10 @@ let engage () =
let set_batch_mode () = batch_mode := true
let toplevel_default_name = DirPath.make [Id.of_string "Top"]
-let toplevel_name = ref (Some toplevel_default_name)
+let toplevel_name = ref toplevel_default_name
let set_toplevel_name dir =
if DirPath.is_empty dir then error "Need a non empty toplevel module name";
- toplevel_name := Some dir
-let unset_toplevel_name () = toplevel_name := None
+ toplevel_name := dir
let remove_top_ml () = Mltop.remove ()
@@ -565,7 +564,6 @@ let parse_args arglist =
if Coq_config.no_native_compiler then
warning "Native compilation was disabled at configure time."
else native_compiler := true
- |"-notop" -> unset_toplevel_name ()
|"-output-context" -> output_context := true
|"-profile-ltac" -> Flags.profile_ltac := true
|"-q" -> no_load_rc ()
@@ -638,7 +636,7 @@ let init_toplevel arglist =
engage ();
if (not !batch_mode || List.is_empty !compile_list)
&& Global.env_is_initial ()
- then Option.iter Declaremods.start_library !toplevel_name;
+ then Declaremods.start_library !toplevel_name;
init_library_roots ();
load_vernac_obj ();
require ();
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 38ceacf5e..66f782ffb 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -30,7 +30,6 @@ let print_usage_channel co command =
\n -R dir coqdir recursively map physical dir to logical coqdir\
\n -Q dir coqdir map physical dir to logical coqdir\
\n -top coqdir set the toplevel name to be coqdir instead of Top\
-\n -notop set the toplevel name to be the empty logical path\
\n -exclude-dir f exclude subdirectories named f for option -R\
\n\
\n -noinit start without loading the Init library\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 08:30:30 +0000