aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/omega/coq_omega.ml12
-rw-r--r--contrib/ring/quote.ml5
-rw-r--r--contrib/ring/ring.ml5
-rw-r--r--contrib/xml/xmlcommand.ml3
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/names.mli4
-rw-r--r--library/declare.ml2
-rw-r--r--library/global.ml4
-rw-r--r--library/library.ml2
-rwxr-xr-xlibrary/nametab.ml40
-rwxr-xr-xlibrary/nametab.mli4
-rw-r--r--parsing/astterm.ml22
-rw-r--r--parsing/coqlib.ml5
-rw-r--r--parsing/pretty.ml5
-rw-r--r--parsing/termast.ml4
-rw-r--r--proofs/tacinterp.ml6
-rw-r--r--tactics/auto.ml8
-rw-r--r--toplevel/vernacentries.ml13
18 files changed, 77 insertions, 69 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index fec7fb701..00ce6d207 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -213,10 +213,11 @@ let recognize_number t =
let constant dir s =
let dir = "Coq"::dir in
+ let id = id_of_string s in
try
- Declare.global_reference_in_absolute_module dir (id_of_string s)
+ Declare.global_reference_in_absolute_module dir id
with Not_found ->
- anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s)))
+ anomaly ("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir id)))
let zarith_constant dir = constant ("Zarith"::dir)
@@ -368,15 +369,16 @@ let build_coq_eq = build_coq_eq_data.eq
open Closure
let make_coq_path dir s =
let dir = "Coq"::dir in
+ let id = id_of_string s in
let ref =
- try Nametab.locate_in_absolute_module dir (id_of_string s)
+ try Nametab.locate_in_absolute_module dir id
with Not_found ->
- anomaly("Coq_omega: cannot find "^(string_of_qualid (make_qualid dir s)))
+ anomaly("Coq_omega: cannot find "^(string_of_qualid(make_qualid dir id)))
in
match ref with
| ConstRef sp -> EvalConstRef sp
| _ -> anomaly ("Coq_omega: "^
- (string_of_qualid (make_qualid dir s))^
+ (string_of_qualid (make_qualid dir id))^
" is not a constant")
let sp_Zs = lazy (make_coq_path ["Zarith";"zarith_aux"] "Zs")
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 44cbd7868..efc8d78d8 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -114,10 +114,11 @@ open Proof_type
let constant dir s =
let dir = "Coq"::"ring"::dir in
+ let id = id_of_string s in
try
- Declare.global_reference_in_absolute_module dir (id_of_string s)
+ Declare.global_reference_in_absolute_module dir id
with Not_found ->
- anomaly ("Quote: cannot find "^(string_of_qualid (make_qualid dir s)))
+ anomaly ("Quote: cannot find "^(string_of_qualid (make_qualid dir id)))
let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm")
let coq_Node_vm = lazy (constant ["Quote"] "Node_vm")
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index b3421c969..7b3b8f6f6 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -27,10 +27,11 @@ let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
let constant dir s =
let dir = "Coq"::"ring"::dir in
+ let id = id_of_string s in
try
- Declare.global_reference_in_absolute_module dir (id_of_string s)
+ Declare.global_reference_in_absolute_module dir id
with Not_found ->
- anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir s)))
+ anomaly ("Ring: cannot find "^(string_of_qualid (make_qualid dir id)))
(* Ring_theory *)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index a3c1af98d..4d4b05d78 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -699,8 +699,7 @@ let print sp fn =
let module N = Names in
let module T = Term in
let module X = Xml in
- let (_,str) = N.repr_qualid sp in
- let id = Names.id_of_string str in
+ let (_,id) = N.repr_qualid sp in
let glob_ref = Nametab.locate sp in
let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
reset_ids () ;
diff --git a/kernel/names.ml b/kernel/names.ml
index fc3453611..83cea889a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -256,7 +256,7 @@ let kind_of_string = function
(*s Section paths *)
-type qualid = string list * string
+type qualid = string list * identifier
let make_qualid p s = (p,s)
let repr_qualid q = q
diff --git a/kernel/names.mli b/kernel/names.mli
index edcadf634..6912d6665 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -60,8 +60,8 @@ val string_of_dirpath : dir_path -> string
(*s Qualified idents are names relative to the current visilibity of names *)
type qualid
-val make_qualid : dir_path -> string -> qualid
-val repr_qualid : qualid -> dir_path * string
+val make_qualid : dir_path -> identifier -> qualid
+val repr_qualid : qualid -> dir_path * identifier
val string_of_qualid : qualid -> string
val pr_qualid : qualid -> std_ppcmds
diff --git a/library/declare.ml b/library/declare.ml
index 57e58256e..853a22d12 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -420,7 +420,7 @@ let dirpath_of_global = function
let is_global id =
try
- let osp = Nametab.locate (make_qualid [] (string_of_id id)) in
+ let osp = Nametab.locate (make_qualid [] id) in
list_prefix_of (dirpath_of_global osp) (Lib.cwd())
with Not_found ->
false
diff --git a/library/global.ml b/library/global.ml
index c07452988..cdc7fdb18 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -63,9 +63,9 @@ let sp_of_global id = Environ.sp_of_global (env_of_safe_env !global_env) id
let qualid_of_global ref =
let sp = sp_of_global ref in
- let s = string_of_id (basename sp) in
+ let id = basename sp in
let rec find_visible dir qdir =
- let qid = make_qualid qdir s in
+ let qid = make_qualid qdir id in
if (try Nametab.locate qid = ref with Not_found -> false) then qid
else match dir with
| [] -> qualid_of_sp sp
diff --git a/library/library.ml b/library/library.ml
index b0c1a2ecd..0ec028963 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -117,7 +117,7 @@ let rec open_module force s =
if force or not m.module_opened then begin
List.iter (fun (m,_,exp) -> if exp then open_module force m) m.module_deps;
open_objects m.module_declarations;
- Nametab.open_module_contents (make_qualid [] s);
+ Nametab.open_module_contents (make_qualid [] (id_of_string s));
m.module_opened <- true
end
diff --git a/library/nametab.ml b/library/nametab.ml
index c8e10a1ed..046a9518c 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -17,22 +17,22 @@ let coq_root = "Coq"
let default_root = "Scratch"
(* Names tables *)
-type cci_table = global_reference Stringmap.t
-type obj_table = (section_path * obj) Stringmap.t
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * obj) Idmap.t
type mod_table = (section_path * module_contents) Stringmap.t
and module_contents = Closed of cci_table * obj_table * mod_table
let empty =
- Closed (Stringmap.empty, Stringmap.empty, Stringmap.empty)
+ Closed (Idmap.empty, Idmap.empty, Stringmap.empty)
let persistent_nametab = ref (empty : module_contents)
let local_nametab = ref (empty : module_contents)
let push_cci (Closed (ccitab, objtab, modtab)) s ref =
- Closed (Stringmap.add s ref ccitab, objtab, modtab)
+ Closed (Idmap.add s ref ccitab, objtab, modtab)
let push_obj (Closed (ccitab, objtab, modtab)) s obj =
- Closed (ccitab, Stringmap.add s obj objtab, modtab)
+ Closed (ccitab, Idmap.add s obj objtab, modtab)
let push_mod (Closed (ccitab, objtab, modtab)) s mc =
(* devrait pas mais ca plante en décommentant la ligne ci-dessous *)
@@ -78,6 +78,7 @@ let push_object sp obj =
let push_module sp mc =
let dir, s = repr_qualid (qualid_of_sp sp) in
+ let s = string_of_id s in
push_mod_absolute dir s (sp,mc);
if List.mem s !roots then
warning ("Cannot allow access to "^s^" by relative paths: it is already registered as a root of the Coq library")
@@ -86,7 +87,7 @@ let push_module sp mc =
(* Sections are not accessible by basename *)
let push_section sp mc =
let dir, s = repr_qualid (qualid_of_sp sp) in
- push_mod_absolute dir s (sp,mc)
+ push_mod_absolute dir (string_of_id s) (sp,mc)
(* This is an entry point for local declarations at toplevel *)
(* Do not use with "open" since it pushes an absolute name too *)
@@ -113,7 +114,7 @@ let locate qid =
let (dir,id) = repr_qualid qid in
let rec search (Closed (ccitab,_,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Stringmap.find id ccitab
+ | [] -> Idmap.find id ccitab
in
try search !local_nametab dir
with Not_found -> search !persistent_nametab dir
@@ -122,16 +123,17 @@ let locate_obj qid =
let (dir,id) = repr_qualid qid in
let rec search (Closed (_,objtab,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Stringmap.find id objtab
+ | [] -> Idmap.find id objtab
in
try search !local_nametab dir
with Not_found -> search !persistent_nametab dir
let locate_module qid =
let (dir,id) = repr_qualid qid in
+ let s = string_of_id id in
let rec search (Closed (_,_,modtab)) = function
| id :: dir' -> search (snd (Stringmap.find id modtab)) dir'
- | [] -> Stringmap.find id modtab
+ | [] -> Stringmap.find s modtab
in
try search !local_nametab dir
with Not_found -> search !persistent_nametab dir
@@ -141,10 +143,10 @@ let locate_constant qid =
| ConstRef sp -> sp
| _ -> raise Not_found
-let sp_of_id _ id = locate (make_qualid [] (string_of_id id))
+let sp_of_id _ id = locate (make_qualid [] id)
let constant_sp_of_id id =
- match locate (make_qualid [] (string_of_id id)) with
+ match locate (make_qualid [] id) with
| ConstRef sp -> sp
| _ -> raise Not_found
@@ -160,7 +162,7 @@ let absolute_reference sp =
exception Found of global_reference
let locate_in_module dir id =
let rec exists_in id (Closed (ccitab,_,modtab)) =
- try raise (Found (Stringmap.find id ccitab))
+ try raise (Found (Idmap.find id ccitab))
with Not_found ->
Stringmap.iter (fun _ (sp,mc) -> exists_in id mc) modtab
in
@@ -174,28 +176,28 @@ let locate_in_module dir id =
let locate_in_absolute_module dir id =
check_absoluteness dir;
- locate_in_module dir (string_of_id id)
+ locate_in_module dir id
(* These are entry points to make the contents of a module/section visible *)
(* in the current env (does not affect the absolute name space `coq_root') *)
let open_module_contents qid =
let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
- Stringmap.iter push_cci_current ccitab;
-(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+ Idmap.iter push_cci_current ccitab;
+(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
Stringmap.iter push_mod_current modtab
let conditional_push ref = push_cci_current ref (* TODO *)
let open_section_contents qid =
let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
- Stringmap.iter push_cci_current ccitab;
-(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+ Idmap.iter push_cci_current ccitab;
+(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
Stringmap.iter push_mod_current modtab
let rec rec_open_module_contents qid =
let _, (Closed (ccitab,objtab,modtab)) = locate_module qid in
- Stringmap.iter push_cci_current ccitab;
-(* Stringmap.iter (fun _ -> Libobject.open_object) objtab;*)
+ Idmap.iter push_cci_current ccitab;
+(* Idmap.iter (fun _ -> Libobject.open_object) objtab;*)
Stringmap.iter
(fun m (sp,_ as mt) ->
push_mod_current m mt;
diff --git a/library/nametab.mli b/library/nametab.mli
index 08aea7ccc..a9a466bb3 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -10,8 +10,8 @@ open Term
(* This module contains the table for globalization, which associates global
names (section paths) to identifiers. *)
-type cci_table = global_reference Stringmap.t
-type obj_table = (section_path * Libobject.obj) Stringmap.t
+type cci_table = global_reference Idmap.t
+type obj_table = (section_path * Libobject.obj) Idmap.t
type mod_table = (section_path * module_contents) Stringmap.t
and module_contents = Closed of cci_table * obj_table * mod_table
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 1e33ea049..a915148a3 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -129,7 +129,11 @@ let interp_qualid p =
| [] -> anomaly "interp_qualid: empty qualified identifier"
| l ->
let p, r = list_chop (List.length l -1) (List.map outnvar l) in
- make_qualid p (List.hd r)
+ make_qualid p (id_of_string (List.hd r))
+
+let maybe_variable = function
+ | [Nvar (_,s)] -> Some s
+ | _ -> None
let ids_of_ctxt ctxt =
Array.to_list
@@ -153,16 +157,16 @@ let maybe_constructor env = function
| IsMutConstruct ((spi,j),cl) ->
IsConstrPat (loc,((spi,j),ids_of_ctxt cl))
| _ ->
- (match repr_qualid qid with
- | [], s ->
+ (match maybe_variable l with
+ | Some s ->
warning ("Defined reference "^(string_of_qualid qid)
^" is here considered as a matching variable");
IsVarPat (loc,s)
| _ -> error ("This reference does not denote a constructor: "
^(string_of_qualid qid)))
with Not_found ->
- match repr_qualid qid with
- | [], s -> IsVarPat (loc,s)
+ match maybe_variable l with
+ | Some s -> IsVarPat (loc,s)
| _ -> error ("Unknown qualified constructor: "
^(string_of_qualid qid)))
@@ -230,7 +234,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc s =
let _ = lookup_id id vars2 in
(* Car Fixpoint met les fns définies tmporairement comme vars de sect *)
try
- let ref = Nametab.locate (make_qualid [] s) in
+ let ref = Nametab.locate (make_qualid [] (id_of_string s)) in
implicits_of_global ref
with _ -> []
in RVar (loc, id), [], imps
@@ -249,7 +253,7 @@ let translate_qualid act qid =
(* Is it a bound variable? *)
try
match repr_qualid qid with
- | [],s -> act.parse_var s, []
+ | [],s -> act.parse_var (string_of_id s), []
| _ -> raise Not_found
with Not_found ->
(* Is it a global reference? *)
@@ -276,7 +280,7 @@ let rawconstr_of_qualid env vars loc qid =
(* Is it a bound variable? *)
try
match repr_qualid qid with
- | [],s -> ast_to_var env vars loc s
+ | [],s -> ast_to_var env vars loc (string_of_id s)
| _ -> raise Not_found
with Not_found ->
(* Is it a global reference? *)
@@ -589,7 +593,7 @@ let ast_adjust_consts sigma =
let id = id_of_string s in
if isMeta s then ast
else if Idset.mem id env then ast
- else adjust_qualid env loc ast (make_qualid [] s)
+ else adjust_qualid env loc ast (make_qualid [] (id_of_string s))
| Node (loc, "QUALID", p) as ast ->
adjust_qualid env loc ast (interp_qualid p)
| Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 94c23ef19..b0a7f3a8a 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -20,10 +20,11 @@ let glob_My_special_variable_nat = ConstRef myvar_path
let reference dir s =
let dir = "Coq"::"Init"::[dir] in
+ let id = id_of_string s in
try
- Nametab.locate_in_absolute_module dir (id_of_string s)
+ Nametab.locate_in_absolute_module dir id
with Not_found ->
- anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir s)))
+ anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id)))
let constant dir s =
Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index af94577af..34d3d2980 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -416,9 +416,8 @@ let print_name qid =
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,str = repr_qualid qid in
if dir <> [] then raise Not_found;
- let name = id_of_string str in
- let (c,typ) = Global.lookup_named name in
- [< print_named_decl (name,c,typ) >]
+ let (c,typ) = Global.lookup_named str in
+ [< print_named_decl (str,c,typ) >]
with Not_found ->
try
let sp = Syntax_def.locate_syntactic_definition qid in
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b1a2d18d1..026e79324 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -94,7 +94,7 @@ let ast_of_ref = function
let ast_of_qualid p =
let dir, s = repr_qualid p in
- let args = List.map nvar (dir@[s]) in
+ let args = List.map nvar (dir@[string_of_id s]) in
ope ("QUALID", args)
(**********************************************************************)
@@ -179,7 +179,7 @@ let rec ast_of_raw = function
| RVar (_,id) ->
let imp =
try
- let ref = Nametab.locate (make_qualid [] (string_of_id id)) in
+ let ref = Nametab.locate (make_qualid [] id) in
implicits_of_global ref
with Not_found -> [] in
ast_of_app imp astf astargs
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c98840d73..9f68b896f 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -186,12 +186,12 @@ let glob_const_nvar loc env qid =
try
(* We first look for a variable of the current proof *)
match repr_qualid qid with
- | [],s ->
- let id = id_of_string s in
+ | [],id ->
(* lookup_value may raise Not_found *)
(match Environ.lookup_named_value id env with
| Some _ -> EvalVarRef id
- | None -> error (s^" does not denote an evaluable constant"))
+ | None -> error ((string_of_id id)^
+ " does not denote an evaluable constant"))
| _ -> raise Not_found
with Not_found ->
try
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7a9ba72b9..e2e719a1d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -421,7 +421,7 @@ let _ =
let hyps = Declare.implicit_section_args ref in
let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
let _,i = repr_qualid qid in
- (id_of_string i, applist (c,section_args))
+ (i, applist (c,section_args))
| _-> bad_vernac_args "HintsResolve") lh in
let dbnames = if l = [] then ["core"] else
List.map (function VARG_IDENTIFIER i -> string_of_id i
@@ -438,7 +438,7 @@ let _ =
List.map (function
| VARG_QUALID qid ->
let _,n = repr_qualid qid in
- (id_of_string n, global qid)
+ (n, global qid)
| _ -> bad_vernac_args "HintsUnfold") lh in
let dbnames = if l = [] then ["core"] else
List.map (function
@@ -462,7 +462,7 @@ let _ =
let c = Declare.constr_of_reference Evd.empty env ref in
let hyps = Declare.implicit_section_args ref in
let section_args = List.map (fun sp -> mkVar (basename sp)) hyps in
- (id_of_string n, applist (c, section_args))
+ (n, applist (c, section_args))
| _ -> bad_vernac_args "HintsImmediate") lh in
let dbnames = if l = [] then ["core"] else
List.map (function
@@ -956,7 +956,7 @@ let cvt_autoArgs =
let interp_to_add gl = function
| (Qualid qid) ->
let _,id = repr_qualid qid in
- (next_ident_away (id_of_string id) (pf_ids_of_hyps gl),
+ (next_ident_away id (pf_ids_of_hyps gl),
Declare.constr_of_reference Evd.empty (Global.env()) (global qid))
| _ -> errorlabstrm "cvt_autoArgs" [< 'sTR "Qualid expected" >]
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 0ce99f904..49042811a 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -181,7 +181,7 @@ let _ =
(fun () -> add_path dir [Nametab.default_root])
| [VARG_STRING dir ; VARG_QUALID alias] ->
let aliasdir,aliasname = repr_qualid alias in
- (fun () -> add_path dir (aliasdir@[aliasname]))
+ (fun () -> add_path dir (aliasdir@[string_of_id aliasname]))
| _ -> bad_vernac_args "ADDPATH")
(* For compatibility *)
@@ -199,7 +199,7 @@ let _ =
| [VARG_STRING dir ; VARG_QUALID alias] ->
let aliasdir,aliasname = repr_qualid alias in
(fun () ->
- let alias = aliasdir@[aliasname] in
+ let alias = aliasdir@[string_of_id aliasname] in
add_rec_path dir alias;
Nametab.push_library_root (List.hd alias))
| _ -> bad_vernac_args "RECADDPATH")
@@ -1369,8 +1369,8 @@ let _ =
let cl_of_qualid qid =
match repr_qualid qid with
- | [], "FUNCLASS" -> Classops.CL_FUN
- | [], "SORTCLASS" -> Classops.CL_SORT
+ | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
+ | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
| _ -> Class.class_of_ref (locate_qualid dummy_loc qid)
let _ =
@@ -1389,8 +1389,7 @@ let _ =
let source = cl_of_qualid qids in
fun () ->
if isid then match repr_qualid qid with
- | [], s ->
- let id = id_of_string s in
+ | [], id ->
Class.try_add_new_identity_coercion id stre source target
| _ -> bad_vernac_args "COERCION"
else
@@ -1686,7 +1685,7 @@ let _ =
if (string_of_id t) = "Tables" then
print_tables ()
else
- mSG(print_name (make_qualid [] (string_of_id t))))
+ mSG(print_name (make_qualid [] t)))
| _ -> bad_vernac_args "TableField")
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:32:11 +0000