aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pmisc.ml3
-rw-r--r--contrib/extraction/extract_env.ml2
-rw-r--r--contrib/extraction/ocaml.ml2
-rw-r--r--contrib/interface/ctast.ml7
-rw-r--r--contrib/interface/name_to_ast.ml6
-rw-r--r--contrib/interface/parse.ml35
-rw-r--r--contrib/interface/pbp.ml2
-rw-r--r--contrib/romega/const_omega.ml2
-rw-r--r--contrib/xml/xmlcommand.ml15
9 files changed, 47 insertions, 27 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 60fe808e0f..ad7779036e 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -143,7 +143,8 @@ let real_subst_in_constr = replace_vars
(* Coq constants *)
let coq_constant d s =
- make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
+ make_path
+ (make_dirpath (List.map id_of_string ("Coq" :: d))) (id_of_string s) CCI
let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
let coq_true = mkMutConstruct ((bool_sp,0),1)
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 68ff965b25..d726d4fa33 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -229,7 +229,7 @@ let _ =
those having an ML extraction. *)
let extract_module m =
- let m = Nametab.locate_loaded_library (Nametab.make_qualid [] m) in
+ let m = Nametab.locate_loaded_library (Nametab.make_short_qualid m) in
let seg = Library.module_segment (Some m) in
let get_reference = function
| sp, Leaf o ->
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1bc47b1e0d..81d77741b0 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -82,7 +82,7 @@ let rename_upper_global id = rename_global (uppercase_id id)
(*s Modules considerations *)
-let module_of_r r = list_last (dirpath (sp_of_r r))
+let module_of_r r = snd (split_dirpath (dirpath (sp_of_r r)))
let string_of_r r = string_of_id (basename (sp_of_r r))
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 4ed6dbcd9e..5b97716fcf 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -16,7 +16,10 @@ type t =
let section_path sl k =
match List.rev sl with
- | s::pa -> make_path (List.rev (List.map id_of_string pa)) (id_of_string s) (kind_of_string k)
+ | s::pa ->
+ make_path
+ (make_dirpath (List.rev (List.map id_of_string pa)))
+ (id_of_string s) (kind_of_string k)
| [] -> invalid_arg "section_path"
let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -53,7 +56,7 @@ let rec ast_to_ct = function
| Coqast.Str (loc,a) -> Str (loc,a)
| Coqast.Path (loc,a) ->
let (sl,bn,pk) = repr_path a in
- Path(loc, (List.map string_of_id sl) @ [string_of_id bn],(* Bidon *) "CCI")
+ Path(loc, (List.map string_of_id (repr_dirpath sl)) @ [string_of_id bn],(* Bidon *) "CCI")
| Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
let loc = function
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 00259ef99f..e4523121c9 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -84,9 +84,9 @@ let implicit_args_to_ast_list sp mipv =
let convert_qualid qid =
let d, id = Nametab.repr_qualid qid in
- match d with
+ match repr_dirpath d with
[] -> nvar id
- | _ -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
+ | d -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
[nvar id]);;
(* This function converts constructors for an inductive definition to a
@@ -228,7 +228,7 @@ let name_to_ast (qid:Nametab.qualid) =
with Not_found ->
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,name = Nametab.repr_qualid qid in
- if dir <> [] then raise Not_found;
+ if dir <> make_dirpath [] then raise Not_found;
let (c,typ) = Global.lookup_named name in
(match c with
None -> make_variable_ast name typ []
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index ff76f2c753..42daf3c191 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -58,7 +58,7 @@ let ctf_FileErrorMessage reqid pps =
function has no effect on parsing *)
let try_require_module import specif name fname =
try Library.require_module (if specif = "UNSPECIFIED" then None
- else Some (specif = "SPECIFICATION")) (Nametab.make_qualid [] (Names.id_of_string name)) fname (import = "IMPORT")
+ else Some (specif = "SPECIFICATION")) (Nametab.make_short_qualid (Names.id_of_string name)) fname (import = "IMPORT")
with
| e -> mSGNL [< 'sTR "Reinterning of "; 'sTR name; 'sTR " failed" >];;
@@ -292,24 +292,35 @@ let parse_file_action reqid file_name =
(* This function is taken from Mltop.add_path *)
let add_path dir coq_dirpath =
- if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+ if coq_dirpath = Names.make_dirpath [] then
+ anomaly "add_path: empty path in library";
+*)
if exists_dir dir then
begin
Library.add_load_path_entry (dir,coq_dirpath);
- Nametab.push_library_root (List.hd coq_dirpath)
+ Nametab.push_library_root coq_dirpath
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >]
+let convert_string d =
+ try Names.id_of_string d
+ with _ -> failwith "caught"
+
let add_rec_path dir coq_dirpath =
- if coq_dirpath = [] then anomaly "add_path: empty path in library";
+(*
+ if coq_dirpath = Names.make_dirpath [] then anomaly "add_path: empty path in library";
+*)
let dirs = all_subdirs dir in
+ let prefix = Names.repr_dirpath coq_dirpath in
if dirs <> [] then
- let convert = List.map Names.id_of_string in
- let dirs = List.map (fun (lp,cp) -> (lp,coq_dirpath@(convert cp))) dirs in
+ let convert_dirs (lp,cp) =
+ (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
+ let dirs = map_succeed convert_dirs dirs in
begin
List.iter Library.add_load_path_entry dirs;
- Nametab.push_library_root (List.hd coq_dirpath)
+ Nametab.push_library_root coq_dirpath
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >];;
@@ -318,7 +329,7 @@ let add_path_action reqid string_arg =
let directory_name = glob string_arg in
let alias = Filename.basename directory_name in
begin
- add_path directory_name [Names.id_of_string alias]
+ add_path directory_name (Names.make_dirpath [Names.id_of_string alias])
end;;
let print_version_action () =
@@ -328,7 +339,7 @@ let print_version_action () =
let load_syntax_action reqid module_name =
mSG [< 'sTR "loading "; 'sTR module_name; 'sTR "... " >];
try
- (let qid = Nametab.make_qualid [] (Names.id_of_string module_name) in
+ (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in
read_module qid;
mSG [< 'sTR "opening... ">];
let fullname = Nametab.locate_loaded_library qid in
@@ -369,9 +380,9 @@ Libobject.relax true;
else
(mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
begin
- add_rec_path (Filename.concat coqdir "theories") [Nametab.coq_root];
- add_path (Filename.concat coqdir "tactics") [Nametab.coq_root];
- add_rec_path (Filename.concat coqdir "contrib") [Nametab.coq_root];
+ add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nametab.coq_root]);
+ add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nametab.coq_root]);
+ add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nametab.coq_root]);
List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
end;
(try
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index cefc9f7e07..4ece713f51 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -176,7 +176,7 @@ let (imply_elim2: pbp_rule) = function
| _ -> None;;
let reference dir s =
- let dir = List.map id_of_string ("Coq"::"Init"::[dir]) in
+ let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::[dir])) in
let id = id_of_string s in
try
Nametab.locate_in_absolute_module dir id
diff --git a/contrib/romega/const_omega.ml b/contrib/romega/const_omega.ml
index c358e593d6..c640383231 100644
--- a/contrib/romega/const_omega.ml
+++ b/contrib/romega/const_omega.ml
@@ -64,7 +64,7 @@ let recognize_number t =
let constant dir s =
try
Declare.global_absolute_reference
- (Names.make_path (List.map Names.id_of_string dir)
+ (Names.make_path (Names.make_dirpath (List.map Names.id_of_string dir))
(Names.id_of_string s) Names.CCI)
with e -> print_endline (String.concat "." dir); print_endline s;
raise e
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 903a8c0ed4..f2de553145 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -100,7 +100,8 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *)
let uri_of_path sp tag =
let module N = Names in
let ext_of_sp sp = ext_of_tag tag in
- let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+ let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
+ let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
"cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
;;
@@ -797,7 +798,8 @@ let mkfilename dn sp ext =
match dn with
None -> None
| Some basedir ->
- let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+ let dir0 = N.extend_dirpath (N.dirpath sp) (N.basename sp) in
+ let dir = List.map N.string_of_id (N.repr_dirpath dir0) in
Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
;;
@@ -918,9 +920,11 @@ with _ -> print_if_verbose ("EXCEPTION RAISED!!!\n");
print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
end
end
- | L.OpenedSection (id,_) ->
+ | L.OpenedSection (dir,_) ->
+ let id = snd (Names.split_dirpath dir) in
print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
- | L.ClosedSection (_,id,state) ->
+ | L.ClosedSection (_,dir,state) ->
+ let id = snd (Names.split_dirpath dir) in
print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
if bprintleaf then
begin
@@ -994,7 +998,8 @@ let printSection id dn =
let rec find_closed_section =
function
[] -> raise Not_found
- | (_,Lib.ClosedSection (_,id',ls))::_ when id' = id -> ls
+ | (_,Lib.ClosedSection (_,dir,ls))::_ when snd (N.split_dirpath dir) = id
+ -> ls
| _::t -> find_closed_section t
in
print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 11:47:27 +0000