1 files changed, 0 insertions, 55 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 0f386ec04..f91d9ff22 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,9 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
-open Names
 open Entries
 open Libnames
 open Constrexpr
@@ -28,8 +25,6 @@ val error_not_a_functor :  module_struct_entry -> 'a
 
 val error_not_equal : module_path -> module_path -> 'a
 
-val error_result_must_be_signature : unit -> 'a
-
 oval error_not_a_modtype_loc : loc -> string -> 'a
 
 val error_not_a_module_loc : loc -> string -> 'a
@@ -41,9 +36,6 @@ val error_with_in_module : unit -> 'a
 val error_application_to_module_type : unit -> 'a
 *)
 
-let error_result_must_be_signature () =
-  error "The result module type must be a signature."
-
 let error_not_a_modtype_loc loc s =
   Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
 
@@ -60,53 +52,6 @@ let error_application_to_module_type loc =
   Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication)
 
 
-
-
-let rec make_mp mp = function
-    [] -> mp
-  | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-
-(*
-(* Since module components are not put in the nametab we try to locate
-the module prefix *)
-exception BadRef
-
-let lookup_qualid (modtype:bool) qid =
-  let rec make_mp mp = function
-      [] -> mp
-    | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
-  in
-  let rec find_module_prefix dir n =
-    if n<0 then raise Not_found;
-    let dir',dir'' = List.chop n dir in
-    let id',dir''' =
-      match dir'' with
-	| hd::tl -> hd,tl
-	| _ -> anomaly "This list should not be empty!"
-    in
-    let qid' = make_qualid dir' id' in
-      try
-	match Nametab.locate qid' with
-	  | ModRef mp -> mp,dir'''
-	  | _ -> raise BadRef
-      with
-	  Not_found -> find_module_prefix dir (pred n)
-  in
-    try Nametab.locate qid
-    with Not_found ->
-      let (dir,id) = repr_qualid qid in
-      let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in
-      let mp =
-	List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir'
-      in
-	if modtype then
-	  ModTypeRef (make_ln mp (label_of_id id))
-	else
-	  ModRef (MPdot (mp,label_of_id id))
-
-*)
-
-
 (* Search for the head of [qid] in [binders].
    If found, returns the module_path/kernel_name created from the dirpath
    and the basename. Searches Nametab otherwise.