summaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml4
-rw-r--r--library/declaremods.ml123
-rw-r--r--library/global.ml21
-rw-r--r--library/global.mli19
-rw-r--r--library/impargs.ml9
-rw-r--r--library/lib.ml24
-rw-r--r--library/lib.mli5
-rw-r--r--library/libnames.ml10
-rw-r--r--library/libnames.mli4
-rw-r--r--library/libobject.ml6
-rw-r--r--library/library.ml53
-rw-r--r--library/library.mli3
-rw-r--r--library/nameops.ml4
13 files changed, 157 insertions, 128 deletions
diff --git a/library/declare.ml b/library/declare.ml
index b1e55c20..81401a8e 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: declare.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
+(* $Id: declare.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
open Pp
open Util
@@ -204,7 +204,7 @@ let hcons_constant_declaration = function
let (hcons1_constr,_) = hcons_constr (hcons_names()) in
DefinitionEntry
{ const_entry_body = hcons1_constr ce.const_entry_body;
- const_entry_type = option_app hcons1_constr ce.const_entry_type;
+ const_entry_type = option_map hcons1_constr ce.const_entry_type;
const_entry_opaque = ce.const_entry_opaque;
const_entry_boxed = ce.const_entry_boxed }
| cd -> cd
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3b2196a5..aac2b599 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 7720 2005-12-24 00:25:55Z herbelin $ i*)
+(*i $Id: declaremods.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
open Pp
open Util
@@ -122,6 +122,18 @@ let msid_of_prefix (_,(mp,sec)) =
anomaly ("Non-empty section in module name!" ^
string_of_mp mp ^ "." ^ string_of_dirpath sec)
+(* Check that a module type is not functorial *)
+
+let rec check_sig env = function
+ | MTBident kn -> check_sig env (Environ.lookup_modtype kn env)
+ | MTBsig _ -> ()
+ | MTBfunsig _ -> Modops.error_result_must_be_signature ()
+
+let rec check_sig_entry env = function
+ | MTEident kn -> check_sig env (Environ.lookup_modtype kn env)
+ | MTEsig _ -> ()
+ | MTEfunsig _ -> Modops.error_result_must_be_signature ()
+ | MTEwith (mte,_) -> check_sig_entry env mte
(* This function checks if the type calculated for the module [mp] is
a subtype of [sub_mtb]. Uses only the global environment. *)
@@ -434,58 +446,47 @@ let rec get_some_body mty env = match mty with
replace_module (get_some_body mty env) id (Environ.lookup_module mp env)
-let intern_args interp_modtype (env,oldargs) (idl,arg) =
+let intern_args interp_modtype (idl,arg) =
let lib_dir = Lib.library_dp() in
let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in
- let mty = interp_modtype env arg in
+ let mty = interp_modtype (Global.env()) arg in
let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
- let mps = List.map (fun mbid -> MPbound mbid) mbids in
let substobjs = get_modtype_substobjs mty in
- let substituted's =
- List.map2
- (fun dir mp -> dir, mp, subst_substobjs dir mp substobjs)
- dirs mps
- in
- List.iter
- (fun (dir, mp, substituted) ->
- do_module false "interp" load_objects 1 dir mp substobjs substituted)
- substituted's;
- let body = Modops.module_body_of_type (get_some_body mty env) in
- let env =
- List.fold_left (fun env mp -> Modops.add_module mp body env) env mps
- in
- env, List.map (fun mbid -> mbid,mty) mbids :: oldargs
-
+ List.map2
+ (fun dir mbid ->
+ Global.add_module_parameter mbid mty;
+ let mp = MPbound mbid in
+ let substituted = subst_substobjs dir mp substobjs in
+ do_module false "interp" load_objects 1 dir mp substobjs substituted;
+ (mbid,mty))
+ dirs mbids
+
let start_module interp_modtype export id args res_o =
let fs = Summary.freeze_summaries () in
- let env = Global.env () in
- let env,arg_entries_revlist =
- List.fold_left (intern_args interp_modtype) (env,[]) args
- in
- let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+ let mp = Global.start_module id in
+ let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
let res_entry_o, sub_body_o = match res_o with
None -> None, None
- | Some (res, true) ->
- Some (interp_modtype env res), None
- | Some (res, false) ->
- (* If the module type is non-restricting, we must translate it
- here to catch errors as early as possible. If it is
- estricting, the kernel takes care of it. *)
- let sub_mte =
- List.fold_right
- (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
- arg_entries
- (interp_modtype env res)
- in
- let sub_mtb =
- Mod_typing.translate_modtype (Global.env()) sub_mte
- in
+ | Some (res, restricted) ->
+ (* we translate the module here to catch errors as early as possible *)
+ let mte = interp_modtype (Global.env()) res in
+ check_sig_entry (Global.env()) mte;
+ if restricted then
+ Some mte, None
+ else
+ let mtb = Mod_typing.translate_modtype (Global.env()) mte in
+ let sub_mtb =
+ List.fold_right
+ (fun (arg_id,arg_t) mte ->
+ let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t
+ in MTBfunsig(arg_id,arg_t,mte))
+ arg_entries mtb
+ in
None, Some sub_mtb
in
- let mp = Global.start_module id arg_entries res_entry_o in
-
let mbids = List.map fst arg_entries in
openmod_info:=(mbids,res_entry_o,sub_body_o);
let prefix = Lib.start_module export id mp fs in
@@ -496,8 +497,8 @@ let start_module interp_modtype export id args res_o =
let end_module id =
let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
- let mp = Global.end_module id in
let mbids, res_o, sub_o = !openmod_info in
+ let mp = Global.end_module id res_o in
begin match sub_o with
None -> ()
@@ -584,7 +585,7 @@ let register_library dir cenv objs digest =
let msid,substitute,keep = objs in
let substobjs = empty_subst, [], msid, substitute in
let substituted = subst_substobjs dir mp substobjs in
- let objects = option_app (fun seg -> seg@keep) substituted in
+ let objects = option_map (fun seg -> seg@keep) substituted in
let modobjs = substobjs, objects in
Hashtbl.add library_cache dir modobjs;
modobjs
@@ -644,13 +645,9 @@ let import_module export mp =
let start_modtype interp_modtype id args =
let fs = Summary.freeze_summaries () in
- let env = Global.env () in
- let env,arg_entries_revlist =
- List.fold_left (intern_args interp_modtype) (env,[]) args
- in
- let arg_entries = List.concat (List.rev arg_entries_revlist) in
- let mp = Global.start_modtype id arg_entries in
+ let mp = Global.start_modtype id in
+ let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
let mbids = List.map fst arg_entries in
openmodtype_info := mbids;
@@ -685,12 +682,11 @@ let end_modtype id =
let declare_modtype interp_modtype id args mty =
let fs = Summary.freeze_summaries () in
- let env = Global.env () in
- let env,arg_entries_revlist =
- List.fold_left (intern_args interp_modtype) (env,[]) args
- in
- let arg_entries = List.concat (List.rev arg_entries_revlist) in
- let base_mty = interp_modtype env mty in
+
+ let _ = Global.start_modtype id in
+ let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
+ let base_mty = interp_modtype (Global.env()) mty in
let entry =
List.fold_right
(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
@@ -730,27 +726,25 @@ let rec get_module_substobjs env = function
let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
-
let fs = Summary.freeze_summaries () in
- let env = Global.env () in
- let env,arg_entries_revlist =
- List.fold_left (intern_args interp_modtype) (env,[]) args
- in
- let arg_entries = List.concat (List.rev arg_entries_revlist) in
+
+ let _ = Global.start_module id in
+ let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in
+
let mty_entry_o, mty_sub_o = match mty_o with
None -> None, None
| (Some (mty, true)) ->
Some (List.fold_right
(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
arg_entries
- (interp_modtype env mty)),
+ (interp_modtype (Global.env()) mty)),
None
| (Some (mty, false)) ->
None,
Some (List.fold_right
(fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte))
arg_entries
- (interp_modtype env mty))
+ (interp_modtype (Global.env()) mty))
in
let mexpr_entry_o = match mexpr_o with
None -> None
@@ -758,12 +752,13 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
Some (List.fold_right
(fun (mbid,mte) me -> MEfunctor(mbid,mte,me))
arg_entries
- (interp_modexpr env mexpr))
+ (interp_modexpr (Global.env()) mexpr))
in
let entry =
{mod_entry_type = mty_entry_o;
mod_entry_expr = mexpr_entry_o }
in
+ let env = Global.env() in
let substobjs =
match entry with
| {mod_entry_type = Some mte} -> get_modtype_substobjs mte
diff --git a/library/global.ml b/library/global.ml
index b4d3a7ff..863d26b7 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: global.ml 8723 2006-04-16 15:51:02Z herbelin $ *)
open Util
open Names
@@ -73,22 +73,27 @@ let add_constraints c = global_env := add_constraints c !global_env
let set_engagement c = global_env := set_engagement c !global_env
-let start_module id params mtyo =
+let start_module id =
let l = label_of_id id in
- let mp,newenv = start_module l params mtyo !global_env in
+ let mp,newenv = start_module l !global_env in
global_env := newenv;
mp
-
-let end_module id =
+
+let end_module id mtyo =
let l = label_of_id id in
- let mp,newenv = end_module l !global_env in
+ let mp,newenv = end_module l mtyo !global_env in
global_env := newenv;
mp
-let start_modtype id params =
+let add_module_parameter mbid mte =
+ let newenv = add_module_parameter mbid mte !global_env in
+ global_env := newenv
+
+
+let start_modtype id =
let l = label_of_id id in
- let mp,newenv = start_modtype l params !global_env in
+ let mp,newenv = start_modtype l !global_env in
global_env := newenv;
mp
diff --git a/library/global.mli b/library/global.mli
index 278b9e65..96965465 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: global.mli 7899 2006-01-20 16:35:03Z barras $ i*)
+(*i $Id: global.mli 8723 2006-04-16 15:51:02Z herbelin $ i*)
(*i*)
open Names
@@ -63,20 +63,13 @@ val set_engagement : engagement -> unit
(* [start_*] functions return the [module_path] valid for components
of the started module / module type *)
-val start_module :
- identifier -> (mod_bound_id * module_type_entry) list
- -> module_type_entry option
- -> module_path
+val start_module : identifier -> module_path
+val end_module : identifier -> module_type_entry option -> module_path
-val end_module :
- identifier -> module_path
+val add_module_parameter : mod_bound_id -> module_type_entry -> unit
-val start_modtype :
- identifier -> (mod_bound_id * module_type_entry) list
- -> module_path
-
-val end_modtype :
- identifier -> kernel_name
+val start_modtype : identifier -> module_path
+val end_modtype : identifier -> kernel_name
(* Queries *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 08ae2aa5..68fc046c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *)
+(* $Id: impargs.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
open Util
open Names
@@ -282,14 +282,15 @@ let compute_mib_implicits kn =
let ar =
Array.to_list
(Array.map (* No need to lift, arities contain no de Bruijn *)
- (fun mip -> (Name mip.mind_typename, None, mip.mind_user_arity))
+ (fun mip -> (Name mip.mind_typename, None, type_of_inductive (mib,mip)))
mib.mind_packets) in
let env_ar = push_rel_context ar env in
let imps_one_inductive i mip =
let ind = (kn,i) in
- ((IndRef ind,auto_implicits env (body_of_type mip.mind_user_arity)),
+ let ar = type_of_inductive (mib,mip) in
+ ((IndRef ind,auto_implicits env ar),
Array.mapi (fun j c -> (ConstructRef (ind,j+1),auto_implicits env_ar c))
- mip.mind_user_lc)
+ mip.mind_nf_lc)
in
Array.mapi imps_one_inductive mib.mind_packets
diff --git a/library/lib.ml b/library/lib.ml
index ee553cad..ba6b9c79 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: lib.ml 7710 2005-12-23 10:16:42Z herbelin $ *)
+(* $Id: lib.ml 8852 2006-05-23 17:52:43Z notin $ *)
open Pp
open Util
@@ -460,7 +460,7 @@ let open_section id =
let discharge_item = function
| ((sp,_ as oname),Leaf lobj) ->
- option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
| _ ->
None
@@ -624,12 +624,30 @@ let reset_initial () =
(* Misc *)
+let mp_of_global ref =
+ match ref with
+ | VarRef id -> fst (current_prefix ())
+ | ConstRef cst -> con_modpath cst
+ | IndRef ind -> ind_modpath ind
+ | ConstructRef constr -> constr_modpath constr
+
+let rec dp_of_mp modp =
+ match modp with
+ | MPfile dp -> dp
+ | MPbound _ | MPself _ -> library_dp ()
+ | MPdot (mp,_) -> dp_of_mp mp
+
let library_part ref =
+ match ref with
+ | VarRef id -> library_dp ()
+ | _ -> dp_of_mp (mp_of_global ref)
+
+let remove_section_part ref =
let sp = Nametab.sp_of_global ref in
let dir,_ = repr_path sp in
match ref with
| VarRef id ->
- anomaly "library_part not supported on local variables"
+ anomaly "remove_section_part not supported on local variables"
| _ ->
if is_dirpath_prefix_of dir (cwd ()) then
(* Not yet (fully) discharged *)
diff --git a/library/lib.mli b/library/lib.mli
index 22b6b6d8..e33c3aca 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: lib.mli 6758 2005-02-20 18:13:28Z herbelin $ i*)
+(*i $Id: lib.mli 8852 2006-05-23 17:52:43Z notin $ i*)
(*i*)
open Util
@@ -122,7 +122,8 @@ val end_compilation : dir_path -> object_prefix * library_segment
val library_dp : unit -> dir_path
(* Extract the library part of a name even if in a section *)
-val library_part : global_reference -> dir_path
+val library_part : global_reference -> dir_path
+val remove_section_part : global_reference -> dir_path
(*s Sections *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 536a382d..48a7565e 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.ml 7052 2005-05-20 15:54:50Z herbelin $ i*)
+(*i $Id: libnames.ml 8768 2006-04-28 14:25:31Z notin $ i*)
open Pp
open Util
@@ -78,6 +78,14 @@ let dirpath_prefix p = match repr_dirpath p with
let is_dirpath_prefix_of d1 d2 =
list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+let chop_dirpath n d =
+ let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in
+ make_dirpath (List.rev d1), make_dirpath (List.rev d2)
+
+let drop_dirpath_prefix d1 d2 =
+ let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
+ make_dirpath (List.rev d)
+
(* To know how qualified a name should be to be understood in the current env*)
let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
diff --git a/library/libnames.mli b/library/libnames.mli
index 06595e81..ab2185a6 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.mli 7052 2005-05-20 15:54:50Z herbelin $ i*)
+(*i $Id: libnames.mli 8768 2006-04-28 14:25:31Z notin $ i*)
(*i*)
open Pp
@@ -53,6 +53,8 @@ val split_dirpath : dir_path -> dir_path * identifier
val extend_dirpath : dir_path -> module_ident -> dir_path
val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+val chop_dirpath : int -> dir_path -> dir_path * dir_path
+val drop_dirpath_prefix : dir_path -> dir_path -> dir_path
val extract_dirpath_prefix : int -> dir_path -> dir_path
val is_dirpath_prefix_of : dir_path -> dir_path -> bool
diff --git a/library/libobject.ml b/library/libobject.ml
index 708c19b1..7f383a3b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: libobject.ml 6748 2005-02-18 22:17:50Z herbelin $ *)
+(* $Id: libobject.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
open Util
open Names
@@ -109,12 +109,12 @@ let declare_object odecl =
anomaly "somehow we got the wrong dynamic object in the classifyfun"
and discharge (oname,lobj) =
if Dyn.tag lobj = na then
- option_app infun (odecl.discharge_function (oname,outfun lobj))
+ option_map infun (odecl.discharge_function (oname,outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the dischargefun"
and exporter lobj =
if Dyn.tag lobj = na then
- option_app infun (odecl.export_function (outfun lobj))
+ option_map infun (odecl.export_function (outfun lobj))
else
anomaly "somehow we got the wrong dynamic object in the exportfun"
diff --git a/library/library.ml b/library/library.ml
index 760b6f07..cfd88ca0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: library.ml 8877 2006-05-30 16:37:04Z notin $ *)
open Pp
open Util
@@ -57,7 +57,6 @@ let canonical_path_name p =
(* We give up to find a canonical name and just simplify it... *)
strip_path p
-
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
match list_filter2 (fun p d -> p = phys_dir) !load_paths with
@@ -65,38 +64,44 @@ let find_logical_path phys_dir =
| _,[] -> Nameops.default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+let is_in_load_paths phys_dir =
+ let dir = canonical_path_name phys_dir in
+ let lp = get_load_paths () in
+ let check_p = fun p -> (String.compare dir p) == 0 in
+ List.exists check_p lp
+
let remove_load_path dir =
load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
let add_load_path (phys_path,coq_path) =
let phys_path = canonical_path_name phys_path in
- match list_filter2 (fun p d -> p = phys_path) !load_paths with
- | _,[dir] ->
- if coq_path <> dir
- (* If this is not the default -I . to coqtop *)
- && not
- (phys_path = canonical_path_name Filename.current_dir_name
- && coq_path = Nameops.default_root_prefix)
- then
- begin
- (* Assume the user is concerned by library naming *)
- if dir <> Nameops.default_root_prefix then
- (Options.if_verbose warning (phys_path^" was previously bound to "
- ^(string_of_dirpath dir)
- ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
- flush_all ());
- remove_load_path phys_path;
- load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
- end
- | _,[] ->
- load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
- | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+ match list_filter2 (fun p d -> p = phys_path) !load_paths with
+ | _,[dir] ->
+ if coq_path <> dir
+ (* If this is not the default -I . to coqtop *)
+ && not
+ (phys_path = canonical_path_name Filename.current_dir_name
+ && coq_path = Nameops.default_root_prefix)
+ then
+ begin
+ (* Assume the user is concerned by library naming *)
+ if dir <> Nameops.default_root_prefix then
+ (Options.if_verbose warning (phys_path^" was previously bound to "
+ ^(string_of_dirpath dir)
+ ^("\nIt is remapped to "^(string_of_dirpath coq_path)));
+ flush_all ());
+ remove_load_path phys_path;
+ load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+ end
+ | _,[] ->
+ load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+ | _ -> anomaly ("Two logical paths are associated to "^phys_path)
let physical_paths (dp,lp) = dp
let load_paths_of_dir_path dir =
fst (list_filter2 (fun p d -> d = dir) !load_paths)
-
+
let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
(************************************************************************)
diff --git a/library/library.mli b/library/library.mli
index f7620682..27ace544 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: library.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id: library.mli 8877 2006-05-30 16:37:04Z notin $ i*)
(*i*)
open Util
@@ -64,6 +64,7 @@ val get_full_load_paths : unit -> (System.physical_path * dir_path) list
val add_load_path : System.physical_path * dir_path -> unit
val remove_load_path : System.physical_path -> unit
val find_logical_path : System.physical_path -> dir_path
+val is_in_load_paths : System.physical_path -> bool
val load_paths_of_dir_path : dir_path -> System.physical_path list
(*s Locate a library in the load paths *)
diff --git a/library/nameops.ml b/library/nameops.ml
index 6db5f75d..1c6a7d56 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: nameops.ml 6205 2004-10-12 10:13:15Z herbelin $ *)
+(* $Id: nameops.ml 8727 2006-04-24 09:48:06Z herbelin $ *)
open Pp
open Util
@@ -138,7 +138,7 @@ let next_ident_away_from id avoid =
let out_name = function
| Name id -> id
- | Anonymous -> anomaly "out_name: expects a defined name"
+ | Anonymous -> failwith "out_name: expects a defined name"
let name_fold f na a =
match na with
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 12:31:15 +0000