diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
tree | 905dbbafa65dd7bf02823318326be2ca389f833f /plugins | |
parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) |
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/extraction/common.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extract_env.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 6 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 2 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 4 | ||||
-rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
-rw-r--r-- | plugins/romega/const_omega.ml | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 12 | ||||
-rw-r--r-- | plugins/syntax/ascii_syntax.ml | 2 | ||||
-rw-r--r-- | plugins/syntax/numbers_syntax.ml | 4 | ||||
-rw-r--r-- | plugins/syntax/r_syntax.ml | 2 | ||||
-rw-r--r-- | plugins/syntax/z_syntax.ml | 2 | ||||
-rw-r--r-- | plugins/xml/cic2acic.ml | 18 | ||||
-rw-r--r-- | plugins/xml/doubleTypeInference.ml | 2 | ||||
-rw-r--r-- | plugins/xml/xmlcommand.ml | 10 |
20 files changed, 49 insertions, 49 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 286c11e5a..073f77403 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -584,7 +584,7 @@ let pp_module mp = the constants are directly turned into chars *) let mk_ind path s = - make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (Label.make s) + make_mind (MPfile (dirpath_of_string path)) DirPath.empty (Label.make s) let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 85b9bde71..e94644821 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl = let rec extract_sfb_spec env mp = function | [] -> [] | (l,SFBconst cb) :: msig -> - let kn = make_con mp Dir_path.empty l in + let kn = make_con mp DirPath.empty l in let s = extract_constant_spec env kn cb in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> - let mind = make_mind mp Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in let s = Sind (mind, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs @@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vc = Array.map (make_con mp Dir_path.empty) vl in + let vc = Array.map (make_con mp DirPath.empty) vl in let ms = extract_sfb env mp all msb in let b = Array.exists Visit.needed_con vc in if all || b then @@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function else ms with Impossible -> let ms = extract_sfb env mp all msb in - let c = make_con mp Dir_path.empty l in + let c = make_con mp DirPath.empty l in let b = Visit.needed_con c in if all || b then let d = extract_constant env c cb in @@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function else ms) | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in - let mind = make_mind mp Dir_path.empty l in + let mind = make_mind mp DirPath.empty l in let b = Visit.needed_ind mind in if all || b then let d = Dind (mind, extract_inductive env mind) in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index dba77b923..7d95d2e17 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1304,9 +1304,9 @@ let inline_test r t = not (is_fix t2) && ml_size t < 12 && is_not_strict t) let con_of_string s = - let null = Dir_path.empty in - match Dir_path.repr (dirpath_of_string s) with - | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id) + let null = DirPath.empty in + match DirPath.repr (dirpath_of_string s) with + | id :: d -> make_con (MPfile (DirPath.make d)) null (Label.of_id id) | [] -> assert false let manual_inline_set = diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index eb166675e..01234aa18 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp = let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l')) in + let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index fbd3fd4ea..dfa5ff6f9 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -650,7 +650,7 @@ and pp_module_type params = function let mp_w = List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in + let r = ConstRef (make_con mp_w DirPath.empty (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 320e0d1fc..aabbdc7a4 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -56,7 +56,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (Id.to_string (List.hd (Dir_path.repr f))) + | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -175,7 +175,7 @@ let add_recursors env kn = make_con_equiv (modpath (user_mind kn)) (modpath (canonical_mind kn)) - Dir_path.empty (Label.of_id id) + DirPath.empty (Label.of_id id) in let mib = Environ.lookup_mind kn env in Array.iter @@ -272,7 +272,7 @@ let safe_pr_long_global r = | _ -> assert false let pr_long_mp mp = - let lid = Dir_path.repr (Nametab.dirpath_of_module mp) in + let lid = DirPath.repr (Nametab.dirpath_of_module mp) in str (String.concat "." (List.rev_map Id.to_string lid)) let pr_long_global ref = pr_path (Nametab.path_of_global ref) @@ -424,7 +424,7 @@ let check_loaded_modfile mp = match base_mp mp with if not (Library.library_is_loaded dp) then begin match base_mp (current_toplevel ()) with | MPfile dp' when dp<>dp' -> - err (str ("Please load library "^(Dir_path.to_string dp^" first."))) + err (str ("Please load library "^(DirPath.to_string dp^" first."))) | _ -> () end | _ -> () @@ -727,7 +727,7 @@ let string_of_modfile mp = let file_of_modfile mp = let s0 = match mp with - | MPfile f -> Id.to_string (List.hd (Dir_path.repr f)) + | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in let s = String.copy (string_of_modfile mp) in diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 1a97689b5..53acccf84 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -46,7 +46,7 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * Dir_path.t * Label.t +val repr_of_r : global_reference -> module_path * DirPath.t * Label.t val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> Label.t val current_toplevel : unit -> module_path diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 4c3c48915..fbb00285c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -81,8 +81,8 @@ type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = match Names.repr_con kn with | MPfile dir, sec_dir, id when - sec_dir = Dir_path.empty && - Dir_path.to_string dir = "Coq.Reals.Rdefinitions" + sec_dir = DirPath.empty && + DirPath.to_string dir = "Coq.Reals.Rdefinitions" -> Label.to_string id | _ -> "constant_not_of_R" diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 69e22da43..99bf66d1f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -460,7 +460,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match wf_rel_expr_opt with | None -> let ltof = - let make_dir l = Dir_path.make (List.rev_map Id.of_string l) in + let make_dir l = DirPath.make (List.rev_map Id.of_string l) in Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e89e2f894..92d2fe680 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -132,7 +132,7 @@ let coq_constant s = Coqlib.init_modules s;; let find_reference sl s = - let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in + let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) let eq = lazy(coq_constant "eq") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index addce6b1c..d5e1ee53a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -50,7 +50,7 @@ let coq_base_constant s = (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; let find_reference sl s = - let dp = Names.Dir_path.make (List.rev_map Id.of_string sl) in + let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) = diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 11281f114..d23a07ba6 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -19,7 +19,7 @@ let meaningful_submodule = [ "Z"; "N"; "Pos" ] let string_of_global r = let dp = Nametab.dirpath_of_global r in - let prefix = match Names.Dir_path.repr dp with + let prefix = match Names.DirPath.repr dp with | [] -> "" | m::_ -> let s = Names.Id.to_string m in diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 6cfac9605..35189f786 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -245,13 +245,13 @@ let my_constant c = lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c) let new_ring_path = - Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"]) let ltac s = - lazy(make_kn (MPfile new_ring_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s)) let znew_ring_path = - Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; @@ -827,10 +827,10 @@ END (***********************************************************************) let new_field_path = - Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) + DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) Dir_path.empty (Label.make s)) + lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index fc64da58e..b6fdf315c 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -16,7 +16,7 @@ open Coqlib exception Non_closed_ascii -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index ef4636699..8d3629d35 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -15,10 +15,10 @@ open Glob_term (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***) -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) -let make_mind mp id = Names.make_mind mp Dir_path.empty (Label.make id) +let make_mind mp id = Names.make_mind mp DirPath.empty (Label.make id) let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = let mp = MPdot (MPfile (make_dir dir), Label.make modname) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 055b99adc..bddca9e65 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -19,7 +19,7 @@ exception Non_closed_number open Glob_term open Bigint -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] let make_path dir id = Libnames.make_path dir (Id.of_string id) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index ca02f61b7..e5e4e9331 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -23,7 +23,7 @@ open Glob_term let binnums = ["Coq";"Numbers";"BinNums"] -let make_dir l = Dir_path.make (List.rev_map Id.of_string l) +let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let positive_path = make_path binnums "positive" diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 90712c473..5f4add47a 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -38,7 +38,7 @@ let get_module_path_of_full_path path = let remove_module_dirpath_from_dirpath ~basedir dir = let module Ln = Libnames in if Ln.is_dirpath_prefix_of basedir dir then - let ids = Names.Dir_path.repr dir in + let ids = Names.DirPath.repr dir in let rec remove_firsts n l = match n,l with (0,l) -> l @@ -48,11 +48,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir = let ids' = List.rev (remove_firsts - (List.length (Names.Dir_path.repr basedir)) + (List.length (Names.DirPath.repr basedir)) (List.rev ids)) in ids' - else Names.Dir_path.repr dir + else Names.DirPath.repr dir ;; @@ -63,7 +63,7 @@ let get_uri_of_var v pvars = function [] -> Errors.error ("Variable "^v^" not found") | he::tl as modules -> - let dirpath = N.Dir_path.make modules in + let dirpath = N.DirPath.make modules in if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then modules else @@ -73,7 +73,7 @@ let get_uri_of_var v pvars = if List.mem v pvars then [] else - search_in_open_sections (N.Dir_path.repr (Lib.cwd ())) + search_in_open_sections (N.DirPath.repr (Lib.cwd ())) in "cic:" ^ List.fold_left @@ -108,21 +108,21 @@ let ext_of_tag = exception FunctorsXMLExportationNotImplementedYet;; let subtract l1 l2 = - let l1' = List.rev (Names.Dir_path.repr l1) in - let l2' = List.rev (Names.Dir_path.repr l2) in + let l1' = List.rev (Names.DirPath.repr l1) in + let l2' = List.rev (Names.DirPath.repr l2) in let rec aux = function he::tl when tl = l2' -> [he] | he::tl -> he::(aux tl) | [] -> assert (l2' = []) ; [] in - Names.Dir_path.make (List.rev (aux l1')) + Names.DirPath.make (List.rev (aux l1')) ;; let token_list_of_path dir id tag = let module N = Names in let token_list_of_dirpath dirpath = - List.rev_map N.Id.to_string (N.Dir_path.repr dirpath) in + List.rev_map N.Id.to_string (N.DirPath.repr dirpath) in token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)] let token_list_of_kernel_name tag = diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml index fcd01569a..c95cf94b6 100644 --- a/plugins/xml/doubleTypeInference.ml +++ b/plugins/xml/doubleTypeInference.ml @@ -20,7 +20,7 @@ let cprop = N.make_con (N.MPfile (Libnames.dirpath_of_string "CoRN.algebra.CLogic")) - (N.Dir_path.empty) + (N.DirPath.empty) (N.Label.make "CProp") ;; diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 91e15e8a6..033c84691 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -46,7 +46,7 @@ let filter_params pvars hyps = let cwd = Lib.cwd () in let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in - aux (Names.Dir_path.repr modulepath) (List.rev pvars) + aux (Names.DirPath.repr modulepath) (List.rev pvars) ;; (* The computation is very inefficient, but we can't do anything *) @@ -62,7 +62,7 @@ let search_variables () = [] -> [] | he::tl as modules -> let one_section_variables = - let dirpath = N.Dir_path.make (modules @ N.Dir_path.repr modulepath) in + let dirpath = N.DirPath.make (modules @ N.DirPath.repr modulepath) in let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in [he,t] in @@ -113,7 +113,7 @@ let theory_filename xml_library_root = match xml_library_root with None -> None (* stdout *) | Some xml_library_root' -> - let toks = List.map N.Id.to_string (N.Dir_path.repr (Lib.library_dp ())) in + let toks = List.map N.Id.to_string (N.DirPath.repr (Lib.library_dp ())) in (* theory from A/B/C/F.v goes into A/B/C/F.theory *) let alltoks = List.rev toks in Some (join_dirs xml_library_root' alltoks ^ ".theory") @@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ; let uri_of_dirpath dir = "/" ^ String.concat "/" - (List.rev_map Names.Id.to_string (Names.Dir_path.repr dir)) + (List.rev_map Names.Id.to_string (Names.DirPath.repr dir)) ;; let _ = @@ -550,5 +550,5 @@ let _ = Library.set_xml_require (fun d -> theory_output_string (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>" - (uri_of_dirpath d) (Names.Dir_path.to_string d))) + (uri_of_dirpath d) (Names.DirPath.to_string d))) ;; |