Some dead code removal + cleanups

  This commit concerns about the first half of the useless code
  mentionned by Oug for coqtop (without plugins). For the moment,
  Oug is used in a mode where any elements mentionned in a .mli
  is considered to be precious. This already allows to detect and
  remove about 600 lines, and more is still to come.

  Among the interesting points, the type Entries.specification_entry
  and its constructors SPExxx were never used. Large parts of cases.ml
  (and hence subtac_cases.ml) were also useless.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7

47 files changed, 53 insertions, 695 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index ccbfbc4c0..591b353db 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -496,9 +496,6 @@ let rec decomp_stack = function
         | _ ->
             Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
   | _ -> None
-let rec decomp_stackn = function
-  | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
-  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
   | [] -> []
@@ -547,8 +544,6 @@ let lift_fconstr k f =
   if k=0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
   if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
-let lift_fconstr_list k l =
-  if k=0 then l else List.map (fun f -> lft_fconstr k f) l
 
 let clos_rel e i =
   match expand_rel i e with
@@ -857,12 +852,6 @@ let get_nth_arg head n stk =
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
-let get_arg h stk =
-  let (depth,stk') = strip_update_shift h stk in
-  match  decomp_stack stk' with
-      Some (v, s') -> (Some (depth,v), s')
-    | None -> (None, zshift depth stk')
-
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9723f2c22..0d2fecfa2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -92,19 +92,6 @@ let insert_pat_alias loc p = function
 (**********************************************************************)
 (* conversion of references                                           *)
 
-let ids_of_ctxt ctxt =
-  Array.to_list
-    (Array.map
-       (function c -> match kind_of_term c with
-	  | Var id -> id
-	  | _ ->
-       error "Arbitrary substitution of references not implemented.")
-     ctxt)
-
-let idopt_of_name = function 
-  | Name id -> Some id
-  | Anonymous -> None
-
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
@@ -574,33 +561,6 @@ let rec rename_rawconstr_var id0 id1 = function
   | RVar(loc,id) when id=id0 -> RVar(loc,id1)
   | c -> map_rawconstr (rename_rawconstr_var id0 id1) c
 
-let rec share_fix_binders n rbl ty def =
-  match ty,def with
-      RProd(_,na0,bk0,t0,b), RLambda(_,na1,bk1,t1,m) ->
-        if not(same_rawconstr t0 t1) then List.rev rbl, ty, def
-        else
-          let (na,b,m) =
-            match na0, na1 with
-                Name id0, Name id1 ->
-                  if id0=id1 then (na0,b,m)
-                  else if not (occur_rawconstr id1 b) then
-                    (na1,rename_rawconstr_var id0 id1 b,m)
-                  else if not (occur_rawconstr id0 m) then
-                    (na1,b,rename_rawconstr_var id1 id0 m)
-                  else (* vraiment pas de chance! *)
-                    failwith "share_fix_binders: capture"
-              | Name id, Anonymous ->
-                  if not (occur_rawconstr id m) then (na0,b,m)
-                  else
-                    failwith "share_fix_binders: capture"
-              | Anonymous, Name id -> 
-                  if not (occur_rawconstr id b) then (na1,b,m)
-                  else
-                    failwith "share_fix_binders: capture"
-              | _ -> (na1,b,m) in
-          share_fix_binders (n-1) ((na,None,t0)::rbl) b m
-    | _ -> List.rev rbl, ty, def
-
 (**********************************************************************)
 (* mapping rawterms to numerals (in presence of coercions, choose the *)
 (* one with no delimiter if possible)                                 *)
@@ -910,13 +870,6 @@ let extern_sort s = extern_rawsort (detype_sort s)
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
-let it_destPLambda n c =
-  let rec aux n nal c =
-    if n=0 then (nal,c) else match c with
-      | PLambda (na,_,c) -> aux (n-1) (na::nal) c
-      | _ -> anomaly "it_destPLambda" in
-  aux n [] c
-
 let rec raw_of_pat env = function
   | PRef ref -> RRef (loc,ref)
   | PVar id -> RVar (loc,id)
@@ -965,9 +918,6 @@ let rec raw_of_pat env = function
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
 
-and raw_of_eqns env constructs consnargsl bl =
-  Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl)
-
 and raw_of_eqn env constr construct_nargs branch =
   let make_pat x env b ids =
     let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 172d032b5..2aee2ea68 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -113,11 +113,6 @@ let explain_internalisation_error e =
   | BadExplicitationNumber (n,po) -> explain_bad_explicitation_number n po in
   pp ++ str "."
 
-let error_unbound_patvar loc n =
-  user_err_loc
-    (loc,"glob_qualid_or_patvar", str "?" ++ pr_patvar n ++ 
-      str " is unbound.")
-
 let error_bad_inductive_type loc =
   user_err_loc (loc,"",str 
     "This should be an inductive type applied to names or \"_\".")
@@ -390,12 +385,6 @@ let apply_scope_env (ids,unb,_,scopes) = function
   | [] -> (ids,unb,None,scopes), []
   | sc::scl -> (ids,unb,sc,scopes), scl
 
-let rec adjust_scopes env scopes = function
-  | [] -> []
-  | a::args ->
-      let (enva,scopes) = apply_scope_env env scopes in
-      enva :: adjust_scopes env scopes args
-
 let rec simple_adjust_scopes n = function
   | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
   | sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
@@ -1210,9 +1199,6 @@ let intern_pattern env patt =
 	user_err_loc (loc,"internalize",explain_internalisation_error e)
 
 
-let intern_ltac isarity ltacvars sigma env c =
-  intern_gen isarity sigma env ~ltacvars:ltacvars c
-
 type manual_implicits = (explicitation * (bool * bool * bool)) list
 
 (*********************************************************************)
@@ -1289,10 +1275,6 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
 let interp_type_evars evdref env ?(impls=([],[])) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
-let interp_constr_judgment_evars evdref env c =
-  Default.understand_judgment_tcc evdref env
-    (intern_constr ( !evdref) env c)
-
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index f9881673d..71f38063a 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -154,16 +154,6 @@ let add_glob_kn loc kn =
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"
 
-let add_local loc id = ()
-(*   let mod_dp,id = repr_path sp in *)
-(*   let mod_dp = remove_sections mod_dp in *)
-(*   let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
-(*   let filepath = string_of_dirpath lib_dp in *)
-(*   let modpath = string_of_dirpath mod_dp_trunc in *)
-(*   let ident = string_of_id id in *)
-(*     dump_string (Printf.sprintf "R%d %s %s %s %s\n"  *)
-(* 		    (fst (unloc loc)) filepath modpath ident ty) *)
-
 let dump_binding loc id = ()
       
 let dump_definition (loc, id) sec s =
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 10ef06993..c4759fa92 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -379,9 +379,6 @@ let rec decomp_stack = function
         | _ ->
             Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s)))
   | _ -> None
-let rec decomp_stackn = function
-  | Zapp v :: s -> if Array.length v = 0 then decomp_stackn s else (v, s)
-  | _ -> assert false
 let array_of_stack s =
   let rec stackrec = function
   | [] -> []
@@ -430,8 +427,6 @@ let lift_fconstr k f =
   if k=0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
   if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
-let lift_fconstr_list k l =
-  if k=0 then l else List.map (fun f -> lft_fconstr k f) l
 
 let clos_rel e i =
   match expand_rel i e with
@@ -741,12 +736,6 @@ let get_nth_arg head n stk =
 
 (* Beta reduction: look for an applied argument in the stack.
    Since the encountered update marks are removed, h must be a whnf *)
-let get_arg h stk =
-  let (depth,stk') = strip_update_shift h stk in
-  match  decomp_stack stk' with
-      Some (v, s') -> (Some (depth,v), s')
-    | None -> (None, zshift depth stk')
-
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 58668c014..0851c7a5f 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -45,14 +45,6 @@ let set_strategy k l =
       else Cmap.add c l !cst_opacity
   | RelKey _ -> Util.error "set_strategy: RelKey"
 
-let set_transparent_const kn =
-  cst_opacity := Cmap.remove kn !cst_opacity
-let set_transparent_var id =
-  var_opacity := Idmap.remove id !var_opacity
-
-let set_opaque_const kn = set_strategy (ConstKey kn) Opaque
-let set_opaque_var id = set_strategy (VarKey id) Opaque
-
 let get_transp_state () =
   (Idmap.fold
     (fun id l ts -> if  l=Opaque then Idpred.remove id ts else ts)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8dde8fb3e..e30fe7737 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -70,14 +70,7 @@ type constant_entry =
 
 (*s Modules *)
 
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEalias of module_path
-  | SPEmodtype of module_struct_entry
-
-and module_struct_entry = 
+type module_struct_entry = 
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
@@ -87,8 +80,6 @@ and with_declaration =
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_structure = (label * specification_entry) list
-
 and module_entry = 
     { mod_entry_type : module_struct_entry option;
       mod_entry_expr : module_struct_entry option}
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 6de90d29c..dc1522dbf 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -69,14 +69,7 @@ type constant_entry =
 
 (*s Modules *)
 
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEalias of module_path
-  | SPEmodtype of module_struct_entry
-
-and module_struct_entry = 
+type module_struct_entry =
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
@@ -86,8 +79,6 @@ and with_declaration =
     With_Module of identifier list * module_path
   | With_Definition of identifier list * constr
 
-and module_structure = (label * specification_entry) list
-
 and module_entry = 
     { mod_entry_type : module_struct_entry option;
       mod_entry_expr : module_struct_entry option}
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4fb5a2b1a..e0f364f2e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -60,12 +60,6 @@ let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
 let push_rec_types (lna,typarray,_) env =
   let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
-    
-let reset_rel_context env =
-  { env with
-    env_rel_context = empty_rel_context;
-    env_rel_val = [];
-    env_nb_rel = 0 }
 
 let fold_rel_context f env ~init =
   let rec fold_right env =
diff --git a/kernel/names.ml b/kernel/names.ml
index 6ee96fddd..953c13aa9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -51,13 +51,7 @@ type name = Name of identifier | Anonymous
 type module_ident = identifier
 type dir_path = module_ident list
 
-module ModIdOrdered = 
-  struct
-    type t = identifier
-    let compare = Pervasives.compare
-  end
-
-module ModIdmap = Map.Make(ModIdOrdered)
+module ModIdmap = Idmap
 
 let make_dirpath x = x
 let repr_dirpath x = x
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 44f5dcb32..44d13a0cb 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -77,14 +77,9 @@ type flags = {fastcomputation : bool}
 
 (*A definition of maps from strings to pro_int31, to be able
   to have any amount of coq representation for the 31bits integers *)
-module OrderedField =
-struct
-  type t = field
-  let compare = compare
-end
-
-module Proactive = Map.Make (OrderedField)
 
+module Proactive =
+  Map.Make (struct type t = field let compare = compare end)
 
 type proactive = entry Proactive.t
 
@@ -98,13 +93,8 @@ type proactive = entry Proactive.t
    a finite type describing the fields to the field of proactive retroknowledge
    (and then to make as many functions as needed in environ.ml) *)
 
-module OrderedEntry =
-struct
-  type t = entry
-  let compare = compare
-end
-
-module Reactive = Map.Make (OrderedEntry)
+module Reactive =
+  Map.Make (struct type t = entry let compare = compare end)
 
 type reactive_end = {(*information required by the compiler of the VM *)
   vm_compiling :
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 65fc78203..24af5da05 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -55,19 +55,17 @@ let cmp_univ_level u v = match u,v with
       else if i1 > i2 then 1
       else compare dp1 dp2
 
-type universe =
-  | Atom of universe_level
-  | Max of universe_level list * universe_level list
-  
-module UniverseOrdered = struct
-  type t = universe_level
-  let compare = cmp_univ_level
-end
-
 let string_of_univ_level = function
   | Set -> "0"
   | Level (d,n) -> Names.string_of_dirpath d^"."^string_of_int n
 
+module UniverseLMap =
+ Map.Make (struct type t = universe_level let compare = cmp_univ_level end)
+
+type universe =
+  | Atom of universe_level
+  | Max of universe_level list * universe_level list
+
 let make_univ (m,n) = Atom (Level (m,n))
 
 let pr_uni_level u = str (string_of_univ_level u)
@@ -121,18 +119,17 @@ type univ_entry =
     Canonical of canonical_arc
   | Equiv of universe_level * universe_level
 
-module UniverseMap = Map.Make(UniverseOrdered)
 
-type universes = univ_entry UniverseMap.t
-		   
+type universes = univ_entry UniverseLMap.t
+
 let enter_equiv_arc u v g =
-  UniverseMap.add u (Equiv(u,v)) g
+  UniverseLMap.add u (Equiv(u,v)) g
 
 let enter_arc ca g =
-  UniverseMap.add ca.univ (Canonical ca) g
+  UniverseLMap.add ca.univ (Canonical ca) g
 
 let declare_univ u g =
-  if not (UniverseMap.mem u g) then
+  if not (UniverseLMap.mem u g) then
     enter_arc (terminal u) g
   else
     g
@@ -162,7 +159,7 @@ let is_univ_variable = function
 
 let type1_univ = Max ([],[Set])
 
-let initial_universes = UniverseMap.empty
+let initial_universes = UniverseLMap.empty
 
 (* Every universe_level has a unique canonical arc representative *)
 
@@ -171,7 +168,7 @@ let initial_universes = UniverseMap.empty
 let repr g u = 
   let rec repr_rec u =
     let a =
-      try UniverseMap.find u g
+      try UniverseLMap.find u g
       with Not_found -> anomalylabstrm "Univ.repr"
 	  (str"Universe " ++ pr_uni_level u ++ str" undefined") 
     in
@@ -443,7 +440,7 @@ let enforce_univ_relation g = function
 (* Merging 2 universe graphs *)
 (*
 let merge_universes sp u1 u2 =
-  UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
+  UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
 *)
 
 
@@ -571,14 +568,14 @@ let no_upper_constraints u cst =
 (* Pretty-printing *)
 
 let num_universes g =
-  UniverseMap.fold (fun _ _ -> succ) g 0
+  UniverseLMap.fold (fun _ _ -> succ) g 0
 
 let num_edges g =
   let reln_len = function
     | Equiv _ -> 1
     | Canonical {lt=lt;le=le} -> List.length lt + List.length le
   in
-  UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0
+  UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0
     
 let pr_arc = function 
   | Canonical {univ=u; lt=[]; le=[]} ->
@@ -594,7 +591,7 @@ let pr_arc = function
       pr_uni_level u  ++ str " = " ++ pr_uni_level v ++ fnl ()
 
 let pr_universes g =
-  let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in
+  let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in
   prlist (function (_,a) -> pr_arc a) graph
     
 let pr_constraints c =
@@ -626,7 +623,7 @@ let dump_universes output g =
 	Printf.fprintf output "%s = %s ;\n"
 	  (string_of_univ_level u) (string_of_univ_level v)
   in
-    UniverseMap.iter dump_arc g 
+    UniverseLMap.iter dump_arc g 
 
 (* Hash-consing *)
 
diff --git a/lib/bigint.ml b/lib/bigint.ml
index a836d0e07..3b974652b 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -167,8 +167,6 @@ let less_than m n =
     (Array.length m = Array.length n && less_than_same_size m n 0 0))
 
 let equal m n = (m = n)
-  
-let less_or_equal_than m n = equal m n or less_than m n
 
 let less_than_shift_pos k m n =
   (Array.length m - k < Array.length n)
@@ -335,9 +333,7 @@ let one = big_of_int 1
 let sub_1 n = sub n one
 let add_1 n = add n one
 let two = big_of_int 2
-let neg_two = big_of_int (-2)
 let mult_2 n = add n n
-let is_zero n = n=zero
 
 let div2_with_rest n =
   let (q,b) = euclid n two in
diff --git a/library/declare.ml b/library/declare.ml
index 2a4b2e403..9e242d2b3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -75,7 +75,7 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (inVariable, outVariable) =
+let (inVariable,_) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -143,7 +143,7 @@ let export_constant cst = Some (dummy_constant cst)
 
 let classify_constant (_,cst) = Substitute (dummy_constant cst)
 
-let (inConstant, outConstant) =
+let (inConstant,_) =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -262,7 +262,7 @@ let dummy_inductive_entry (_,m) = ([],{
 
 let export_inductive x = Some (dummy_inductive_entry x)
 
-let (inInductive, outInductive) =
+let (inInductive,_) =
   declare_object {(default_object "INDUCTIVE") with 
     cache_function = cache_inductive;
     load_function = load_inductive;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 129ea4ef2..52fa94569 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -114,11 +114,6 @@ let mp_of_kn kn =
     else
       anomaly ("Non-empty section in module name!" ^ string_of_kn kn)
 
-let is_bound mp =
-  match mp with
-    | MPbound _ -> true
-    | _ -> false
-
 let dir_of_sp sp = 
   let dir,id = repr_path sp in
     extend_dirpath dir id
@@ -490,7 +485,7 @@ let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,out_modkeep) = 
+let (in_modkeep,_) =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
@@ -575,7 +570,7 @@ let classify_modtype (_,(_,substobjs)) =
   Substitute (None,substobjs)
 
 
-let (in_modtype,out_modtype) =
+let (in_modtype,_) =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
@@ -859,7 +854,7 @@ let subst_import (_,subst,(export,mp as obj)) =
     if mp'==mp then obj else
       (export,mp')
 	
-let (in_import,out_import) = 
+let (in_import,_) =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
diff --git a/library/decls.ml b/library/decls.ml
index 8a67de4ec..5a8729215 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -70,7 +70,3 @@ let last_section_hyps dir =
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
     ~init:[]
-
-let is_section_variable = function
-  | VarRef _ -> true
-  | _ -> false
diff --git a/library/goptions.ml b/library/goptions.ml
index b614ed34a..b5a8b00ea 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -77,8 +77,7 @@ module MakeTable =
       if List.mem_assoc nick !A.table then
 	error "Sorry, this table name is already used"
 
-    module MyType = struct type t = A.t let compare = Pervasives.compare end
-    module MySet = Set.Make(MyType)
+    module MySet = Set.Make (struct type t = A.t let compare = compare end)
 
     let t = ref (MySet.empty : MySet.t)
 
@@ -219,8 +218,8 @@ type 'a option_sig = {
 
 type option_type = bool * (unit -> value) -> (value -> unit) 
 
-module Key = struct type t = option_name let compare = Pervasives.compare end
-module OptionMap = Map.Make(Key)
+module OptionMap =
+  Map.Make (struct  type t = option_name let compare = compare end)
 
 let value_tab = ref OptionMap.empty
 
diff --git a/library/heads.ml b/library/heads.ml
index 1b1dba43f..ea3acbbe8 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -39,12 +39,8 @@ type head_approximation =
 
 (** Registration as global tables and rollback. *)
 
-module Evalreford = struct
-  type t = evaluable_global_reference
-  let compare = Pervasives.compare
-end
-
-module Evalrefmap = Map.Make(Evalreford)
+module Evalrefmap =
+  Map.Make (struct type t = evaluable_global_reference let compare = compare end)
 
 let head_map = ref Evalrefmap.empty
 
diff --git a/library/libnames.ml b/library/libnames.ml
index f0fcd94c9..44da7b6de 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -66,8 +66,6 @@ module RefOrdered =
 module Refset = Set.Make(RefOrdered)
 module Refmap = Map.Make(RefOrdered)
 
-let inductives_table = ref Indmap.empty
-
 (**********************************************)
 
 let pr_dirpath sl = (str (string_of_dirpath sl))
diff --git a/library/libobject.mli b/library/libobject.mli
index 61e650e6b..d104635cd 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -102,7 +102,7 @@ val ident_subst_function : object_name * substitution * 'a -> 'a
 
 type obj
 
-val declare_object : 
+val declare_object :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
 val object_tag : obj -> string
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 66fc4c253..8db62c392 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -33,10 +33,6 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
-let mk_lam = function
-    ([],c) -> c
-  | (bl,c) -> CLambdaN(constr_loc c, bl,c)
-
 let loc_of_binder_let = function
   | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
   | LocalRawDef ((loc,_),_)::_ -> loc
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ec1e7415b..f656fb32e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -120,11 +120,6 @@ let test_plurial_form = function
    "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
 
-let no_coercion loc (c,x) =
-  if c then Util.user_err_loc
-    (loc,"no_coercion",str"No coercion allowed here.");
-  x
-
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 3a57fd545..814236835 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -71,10 +71,6 @@ let error_expect_no_argument loc =
 let nmtoken (loc,a) =
   try int_of_string a
   with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.")
-  
-let interp_xml_attr_qualid = function
-  | "uri", s -> qualid_of_string s
-  | _ -> error "Ill-formed xml attribute"
 
 let get_xml_attr s al = 
   try List.assoc s al
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 65b3a075e..03c704758 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -16,9 +16,6 @@ open Q_util
 open Q_coqast
 open Argextend
 
-let loc = Util.dummy_loc
-let default_loc = <:expr< Util.dummy_loc >>
-
 type grammar_tactic_production_expr =
   | TacTerm of string
   | TacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index f661800a1..dd6b9e8bf 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -16,9 +16,6 @@ open Q_util
 open Q_coqast
 open Argextend
 
-let loc = Util.dummy_loc
-let default_loc = <:expr< Util.dummy_loc >>
-
 type grammar_tactic_production_expr =
   | VernacTerm of string
   | VernacNonTerm of Util.loc * Genarg.argument_type * MLast.expr * string option
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 26507a1ca..1e5722ef1 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -50,9 +50,6 @@ let make_anonymous_patvars =
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
 
-let push_rel_defs =
-  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
-
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
@@ -152,8 +149,6 @@ and pattern_continuation =
 
 let start_history n = Continuation (n, [], Top)
 
-let initial_history = function Continuation (_,[],Top) -> true | _ -> false
-
 let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
@@ -392,9 +387,6 @@ let map_tomatch_type f = function
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
 
-let lift_tomatch n ((current,typ),info) =
-  ((lift n current,lift_tomatch_type n typ),info)
-
 (**********************************************************************)
 (* Utilities on patterns *)
 
@@ -407,12 +399,6 @@ let alias_of_pat = function
   | PatVar (_,name) -> name
   | PatCstr(_,_,_,name) -> name
 
-let unalias_pat = function
-  | PatVar (c,name) as p ->
-      if name = Anonymous then p else PatVar (c,Anonymous)
-  | PatCstr(a,b,c,name) as p ->
-      if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
-
 let remove_current_pattern eqn =
   match eqn.patterns with
     | pat::pats ->
@@ -581,9 +567,6 @@ let replace_tomatch n c =
       ::(replrec (depth+1) rest) in
   replrec 0
 
-let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
-let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
-
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l)::rest ->
@@ -1319,99 +1302,6 @@ let matx_of_eqns env eqns =
 (************************************************************************)
 (* preparing the elimination predicate if any                          *)
 
-let build_expected_arity env isevars isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_)) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args)) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),k,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs)))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8451d1285..70b201a6e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -124,9 +124,6 @@ let make_anonymous_patvars n =
 (* Environment management *)
 let push_rels vars env = List.fold_right push_rel vars env
 
-let push_rel_defs =
-  List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
-
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
 
@@ -210,8 +207,6 @@ and pattern_continuation =
 
 let start_history n = Continuation (n, [], Top)
 
-let initial_history = function Continuation (_,[],Top) -> true | _ -> false
-
 let feed_history arg = function
   | Continuation (n, l, h) when n>=1 ->
       Continuation (n-1, arg :: l, h)
@@ -452,9 +447,6 @@ let map_tomatch_type f = function
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
 
-let lift_tomatch n ((current,typ),info) =
-  ((lift n current,lift_tomatch_type n typ),info)
-
 (**********************************************************************)
 (* Utilities on patterns *)
 
@@ -467,12 +459,6 @@ let alias_of_pat = function
   | PatVar (_,name) -> name
   | PatCstr(_,_,_,name) -> name
 
-let unalias_pat = function
-  | PatVar (c,name) as p ->
-      if name = Anonymous then p else PatVar (c,Anonymous)
-  | PatCstr(a,b,c,name) as p ->
-      if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
-
 let remove_current_pattern eqn =
   match eqn.patterns with
     | pat::pats ->
@@ -658,9 +644,6 @@ let replace_tomatch n c =
       :: replrec (depth+1) rest in
   replrec 0
 
-let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
-let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
-
 let rec liftn_tomatch_stack n depth = function
   | [] -> []
   | Pushed ((c,tm),l,dep)::rest ->
@@ -1283,102 +1266,6 @@ let matx_of_eqns env tomatchl eqns =
       rhs = rhs }
   in List.map build_eqn eqns
 
-(************************************************************************)
-(* preparing the elimination predicate if any                          *)
-
-let build_expected_arity env evdref isdep tomatchl =
-  let cook n = function
-    | _,IsInd (_,IndType(indf,_),_) ->
-        let indf' = lift_inductive_family n indf in
-	Some (build_dependent_inductive env indf', fst (get_arity env indf'))
-    | _,NotInd _ -> None
-  in
-  let rec buildrec n env = function
-    | [] -> new_Type ()
-    | tm::ltm ->
-	match cook n tm with
-	  | None -> buildrec n env ltm
-	  | Some (ty1,aritysign) ->
-	      let rec follow n env = function
-		| d::sign ->
-		    mkProd_or_LetIn_name env
-		      (follow (n+1) (push_rel d env) sign) d
-		| [] ->
-		    if isdep then
-		      mkProd (Anonymous, ty1, 
-			      buildrec (n+1)
-				(push_rel_assum (Anonymous, ty1) env)
-				ltm)
-		    else buildrec n env ltm
-	      in follow n env (List.rev aritysign)
-  in buildrec 0 env tomatchl
-
-let extract_predicate_conclusion isdep tomatchl pred =
-  let cook = function
-    | _,IsInd (_,IndType(_,args),_) -> Some (List.length args)
-    | _,NotInd _ -> None in
-  let rec decomp_lam_force n l p =
-    if n=0 then (l,p) else
-    match kind_of_term p with
-      | Lambda (na,_,c) -> decomp_lam_force (n-1) (na::l) c
-      | _ -> (* eta-expansion *)
-          let na = Name (id_of_string "x") in
-          decomp_lam_force (n-1) (na::l) (applist (lift 1 p, [mkRel 1])) in
-  let rec buildrec allnames p = function
-    | [] -> (List.rev allnames,p)
-    | tm::ltm ->
-	match cook tm with
-	  | None -> 
-              let p = 
-                (* adjust to a sign containing the NotInd's *)
-                if isdep then lift 1 p else p in
-              let names = if isdep then [Anonymous] else [] in
-              buildrec (names::allnames) p ltm
-	  | Some n ->
-              let n = if isdep then n+1 else n in
-              let names,p = decomp_lam_force n [] p in
-              buildrec (names::allnames) p ltm
-  in buildrec [] pred tomatchl
-
-let set_arity_signature dep n arsign tomatchl pred x =
-  (* avoid is not exhaustive ! *)
-  let rec decomp_lam_force n avoid l p =
-    if n = 0 then (List.rev l,p,avoid) else
-    match p with
-      | RLambda (_,(Name id as na),_,_,c) -> 
-          decomp_lam_force (n-1) (id::avoid) (na::l) c
-      | RLambda (_,(Anonymous as na),_,_,c) -> decomp_lam_force (n-1) avoid (na::l) c
-      | _ ->
-          let x = next_ident_away (id_of_string "x") avoid in
-          decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-          (* eta-expansion *)
-            (let a = RVar (dummy_loc,x) in
-             match p with
-               | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-               | _ -> (RApp (dummy_loc,p,[a]))) in
-  let rec decomp_block avoid p = function
-    | ([], _) -> x := Some p
-    | ((_,IsInd (_,IndType(indf,realargs),_))::l),(y::l')  ->
-	let (ind,params) = dest_ind_family indf in
-        let (nal,p,avoid') = decomp_lam_force (List.length realargs) avoid [] p 
-        in
-        let na,p,avoid' = 
-          if dep then decomp_lam_force 1 avoid' [] p else [Anonymous],p,avoid'
-        in 
-        y :=
-        (List.hd na,
-         if List.for_all ((=) Anonymous) nal then
-           None
-         else
-           Some (dummy_loc, ind, (List.map (fun _ -> Anonymous) params)@nal));
-        decomp_block avoid' p (l,l')
-    | (_::l),(y::l') ->
-        y := (Anonymous,None);
-        decomp_block avoid p (l,l')
-    | _ -> anomaly "set_arity_signature"
-  in
-  decomp_block [] pred (tomatchl,arsign)
-
 (***************** Building an inversion predicate ************************)
 
 (* Let "match t1 in I1 u11..u1n_1 ... tm in Im um1..umn_m with ... end : T"
@@ -1754,11 +1641,6 @@ let prepare_predicate_from_arsign_tycon loc env tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
-let is_dependent_on_rel x t =
-  match kind_of_term x with
-      Rel n -> not (noccur_with_meta n n t)
-    | _ -> false
-
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred =
   match pred with
   (* No type annotation *)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index b0554540a..11d6ed093 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -68,8 +68,6 @@ module Bijint = struct
 	(let v = Array.make (b.s + 8) (x,y) in Array.blit b.v 0 v 0 b.s; v)
       else b.v in
     v.(b.s) <- (x,y); { v = v; s = b.s+1; inv = Gmap.add x b.s b.inv }
-  let replace n x y b =
-    let v = Array.copy b.v in v.(n) <- (x,y); { b with v = v }
   let dom b = Gmap.dom b.inv
 end
 
@@ -138,8 +136,6 @@ let coercion_info coe = Gmap.find coe !coercion_tab
 
 let coercion_exists coe = Gmap.mem coe !coercion_tab
 
-let coercion_params coe_info = coe_info.coe_param
-
 (* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
 
 let find_class_type env sigma t =
@@ -383,7 +379,7 @@ let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) =
 	  discharge_cl clt,
           n + ps)
 
-let (inCoercion,outCoercion) =
+let (inCoercion,_) =
   declare_object {(default_object "COERCION") with 
     load_function = load_coercion;
     cache_function = cache_coercion;
@@ -395,9 +391,6 @@ let (inCoercion,outCoercion) =
 let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps =
   Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps))
 
-let coercion_strength v = v.coe_strength
-let coercion_identity v = v.coe_is_identity
-
 (* For printing purpose *)
 let get_coercion_value v = v.coe_value
 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 69b5db5e6..576e217aa 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -32,7 +32,6 @@ open Coercion.Default
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
-let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
 let pf_concl gl = gl.it.evar_concl
 
 (******************************************************************)
@@ -167,8 +166,6 @@ let mentions clenv mv0 =
     meta_exists menrec mlist
   in menrec
 
-let clenv_defined clenv mv = meta_defined clenv.evd mv
-
 let error_incompatible_inst clenv mv  =
   let na = meta_name clenv.evd mv in
   match na with
@@ -197,8 +194,6 @@ let clenv_assign mv rhs clenv =
     error "clenv_assign: undefined meta"
 
 
-let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
-
 
 (* [clenv_dependent hyps_only clenv]
  * returns a list of the metavars which appear in the template of clenv,
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3a5f35125..f8545fdc9 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -73,11 +73,6 @@ module Default = struct
   (* Typing operations dealing with coercions *)
   exception NoCoercion
 
-  let whd_app_evar sigma t =
-    match kind_of_term t with
-      | App (f,l) -> mkApp (whd_evar sigma f,l)
-      | _ -> whd_evar sigma t
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -156,7 +151,6 @@ module Default = struct
 	    inh_tosort_force loc env evd j
 
   let inh_coerce_to_base loc env evd j = (evd, j)
-
   let inh_coerce_to_prod loc env evd t = (evd, t)
 
   let inh_coerce_to_fail env evd rigidonly v t c1 =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d455ec6fe..1a7bb2c6c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -261,10 +261,6 @@ let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
  * operations on the evar constraints *
  *------------------------------------*)
 
-let is_pattern inst =
-  array_for_all (fun a -> isRel a || isVar a) inst &&
-  array_distinct inst
-
 (* Pb: defined Rels and Vars should not be considered as a pattern... *)
 (*
 let is_pattern inst =
@@ -275,19 +271,6 @@ let is_pattern inst =
   is_hopat [] (Array.to_list inst)
 *)
 
-let evar_well_typed_body evd ev evi body =
-  try
-    let env = evar_unfiltered_env evi in
-    let ty = evi.evar_concl in
-    Typing.check env ( evd) body ty;
-    true
-  with e ->
-    pperrnl
-      (str "Ill-typed evar instantiation: " ++ fnl() ++
-       pr_evar_defs evd ++ fnl() ++
-       str "----> " ++ int ev ++ str " := " ++
-       print_constr body);
-    false
 
 (* We have x1..xq |- ?e1 and had to solve something like 
  * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some 
@@ -807,12 +790,6 @@ let solve_evar_evar f env evd ev1 ev2 =
   with CannotProject projs2 ->
   postpone_evar_evar env evd projs1 ev1 projs2 ev2
 
-let expand_rhs env sigma subst rhs =
-  let d = (named_hd env rhs Anonymous,Some rhs,get_type_of env sigma rhs) in
-  let rhs' = lift 1 rhs in
-  let f (id,(idc,t)) = (id,(idc,replace_term rhs' (mkRel 1) (lift 1 t))) in
-  push_rel d env, List.map f subst, mkRel 1
-
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0f2f4655b..500e19002 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -177,11 +177,8 @@ type sort_constraint =
   | SortVar of sort_var list * sort_var list (* (leq,geq) *)
   | EqSort of sort_var
 
-module UniverseOrdered = struct
-  type t = Univ.universe
-  let compare = Pervasives.compare
-end
-module UniverseMap = Map.Make(UniverseOrdered)
+module UniverseMap =
+  Map.Make (struct type t = Univ.universe let compare = compare end)
 
 type sort_constraints = sort_constraint UniverseMap.t
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d3bbce9e3..55df4b185 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -109,19 +109,12 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-module CstOrdered =
-  struct
-    type t = constant
-    let compare = Pervasives.compare
-  end
-module Cstmap = Map.Make(CstOrdered)
+let eval_table = ref Cmap.empty
 
-let eval_table = ref Cstmap.empty
-
-type frozen = (int * constant_evaluation) Cstmap.t
+type frozen = (int * constant_evaluation) Cmap.t
 
 let init () =
-  eval_table := Cstmap.empty
+  eval_table := Cmap.empty
 
 let freeze () =
   !eval_table
@@ -272,10 +265,10 @@ let compute_consteval sigma env ref =
 let reference_eval sigma env = function
   | EvalConst cst as ref -> 
       (try
-	 Cstmap.find cst !eval_table
+	 Cmap.find cst !eval_table
        with Not_found -> begin
 	 let v = compute_consteval sigma env ref in
-	 eval_table := Cstmap.add cst v !eval_table;
+	 eval_table := Cmap.add cst v !eval_table;
 	 v
        end)
   | ref -> compute_consteval sigma env ref
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e7137787b..907995c54 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -61,8 +61,6 @@ type pri_auto_tactic = {
 
 type hint_entry = global_reference option * pri_auto_tactic
 
-let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2
-
 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2
 
 let insert v l = 
@@ -116,19 +114,6 @@ let is_transparent_gr (ids, csts) = function
   | VarRef id -> Idpred.mem id ids
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
-      
-let fmt_autotactic =
-  function
-  | Res_pf (c,clenv) -> (str"apply " ++ pr_lconstr c)
-  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_lconstr c)
-  | Give_exact c -> (str"exact " ++ pr_lconstr c)
-  | Res_pf_THEN_trivial_fail (c,clenv) -> 
-      (str"apply " ++ pr_lconstr c ++ str" ; trivial")
-  | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
-  | Extern tac -> 
-      (str "(external) " ++ Pptactic.pr_glob_tactic (Global.env()) tac)
-
-let pr_autotactic = fmt_autotactic
 
 module Hint_db = struct
 
@@ -467,7 +452,7 @@ let classify_autohint (_,((local,name,hintlist) as obj)) =
 let export_autohint ((local,name,hintlist) as obj) =
   if local then None else Some obj
 
-let (inAutoHint,outAutoHint) =
+let (inAutoHint,_) =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
 		    load_function = (fun _ -> cache_autohint);
@@ -714,9 +699,6 @@ let print_searchtable () =
 
 let priority l = List.filter (fun (_,hint) -> hint.pri = 0) l
 
-let select_unfold_extern =
-  List.filter (function (_,{code = (Unfold_nth _ | Extern _)}) -> true | _ -> false)
-
 (* tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds oftener) *)
 
@@ -1081,10 +1063,6 @@ type autoArguments =
   | UsingTDB       
   | Destructing   
 
-let keepAfter tac1 tac2 = 
-  (tclTHEN tac1 
-     (function g -> tac2 [pf_last_hyp g] g))
-
 let compileAutoArg contac = function
   | Destructing -> 
       (function g -> 
@@ -1139,8 +1117,6 @@ let search_superauto n to_add argl g =
 let superauto n to_add argl  = 
   tclTRY (tclCOMPLETE (search_superauto n to_add argl))
 
-let default_superauto g = superauto !default_search_depth [] [] g
-
 let interp_to_add gl r =
   let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
   let id = id_of_global r in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 68c61bca0..f916e0a3e 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -214,7 +214,7 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let (inHintRewrite,outHintRewrite)=
+let (inHintRewrite,_)=
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
        Libobject.cache_function = cache_hintrewrite;
        Libobject.load_function = (fun _ -> cache_hintrewrite);
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c28f214c7..31ffc8897 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -60,7 +60,6 @@ let e_give_exact flags c gl =
     else exact_check c gl
 (*   let t1 = (pf_type_of gl c) in *)
 (*     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
-      
 let assumption flags id = e_give_exact flags (mkVar id)
 
 open Unification
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 2701566ed..02dace837 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -182,11 +182,6 @@ let interp_constr_or_thesis check_sort sigma env = function
     Thesis n -> Thesis n
   | This c -> This (interp_constr check_sort sigma env c)
 
-let type_tester_var body typ = 
-  raw_app(dummy_loc,
-       RLambda(dummy_loc,Anonymous,Explicit,typ,
-	       RSort (dummy_loc,RProp Null)),body)
-
 let abstract_one_hyp inject h raw = 
   match h with 
       Hvar (loc,(id,None)) ->  
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 967bc88e8..ef2f77069 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -487,9 +487,6 @@ let thus_tac c ctyp submetas gls =
 
 (* general forward step *)
 
-
-let anon_id_base = id_of_string "__" 
-
 let mk_stat_or_thesis info gls = function  
     This c -> c
   | Thesis (For _ ) -> 
@@ -843,12 +840,6 @@ let rec constr_trees (main_ind,wft) ind =
 	  constr_trees (None,itree) ind
     | _,constrs -> main_ind,constrs
 
-let constr_args rp constr =
-  let main_ind,constrs = constr_trees rp (fst constr) in
-  let ctree = constrs.(pred (snd constr)) in
-    array_map_to_list (fun t -> main_ind,t) 
-      (snd (Rtree.dest_node ctree))
-
 let ind_args rp ind =
     let main_ind,constrs = constr_trees rp ind in
     let args ctree =     
@@ -1212,8 +1203,6 @@ let pop_one (id,stack) =
 let pop_stacks stacks =
   List.map pop_one stacks
 
-let patvar_base = id_of_string "__"
-
 let hrec_for fix_id per_info gls obj_id =
   let obj=mkVar obj_id in
   let typ=pf_get_hyp_typ gls obj_id in
@@ -1392,15 +1381,6 @@ let end_tac et2 gls =
 
 (* escape *)
 
-let rec abstract_metas n avoid head = function
-    [] -> 1,head,[]
-  | (meta,typ)::rest -> 
-      let id = next_ident_away (id_of_string "_sbgl") avoid in
-      let p,term,args = abstract_metas (succ n) (id::avoid) head rest in 
-	succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term),
-      (mkMeta n)::args 
-
-    
 let escape_tac gls =  tcl_erase_info gls
 
 (* General instruction engine *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 35d2e1324..b37212d9d 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -175,10 +175,6 @@ let init () = Nbtermdn.empty tactab
 let freeze () = Nbtermdn.freeze tactab
 let unfreeze fs = Nbtermdn.unfreeze fs tactab
 
-let rollback f x =
-  let fs = freeze() in 
-  try f x with e -> (unfreeze fs; raise e)
-
 let add (na,dd) =
   let pat = match dd.d_pat with
     | HypLocation(_,p,_) -> p.d_typ
@@ -202,8 +198,6 @@ let _ =
 let forward_subst_tactic = 
   ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
 
-let set_extern_subst_tactic f = forward_subst_tactic := f
-
 let cache_dd (_,(_,na,dd)) =
   try 
     add (na,dd)
@@ -223,7 +217,7 @@ let subst_dd (_,subst,(local,na,dd)) =
     d_pri = dd.d_pri; 
     d_code = !forward_subst_tactic subst dd.d_code })
 
-let (inDD,outDD) =
+let (inDD,_) =
   declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
@@ -330,7 +324,6 @@ let destructHyp discard id gls =
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
   tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls
 
-let cDHyp id gls = destructHyp true id gls
 let dHyp id gls = destructHyp false id gls
 
 let h_destructHyp b id =
@@ -349,8 +342,6 @@ let dConcl gls =
 
 let h_destructConcl = abstract_tactic TacDestructConcl dConcl
 
-let to2Lists (table : t) = Nbtermdn.to2lists table
-
 let rec search n =
   if n=0 then error "Search has reached zero.";
   tclFIRST
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5e4f847fa..09fc808c6 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -207,8 +207,6 @@ let e_possible_resolve mod_delta db_list local_db gl =
 	(fst (head_constr_bound gl)) gl)
   with Bound | Not_found -> []
 
-let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
-
 let find_first_goal gls = 
   try first_goal gls with UserError _ -> assert false
 
@@ -324,8 +322,6 @@ let make_initial_state n gl dblist localdb =
     dblist = dblist;
     localdb = [localdb] }
 
-let debug_depth_first = Search.debug_depth_first
-
 let e_depth_search debug p db_list local_db gl =
   try
     let tac = if debug then Search.debug_depth_first else Search.depth_first in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 99767afc0..99216a127 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -84,11 +84,6 @@ let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
 let is_applied_setoid_relation = ref (fun _ -> false)
 let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation
 
-let is_applied_relation t =
-  match kind_of_term t with
-  | App (c, args) when Array.length args >= 2 -> true
-  | _ -> false
-
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
@@ -230,24 +225,14 @@ let conditional_rewrite lft2rgt tac (c,bl) =
     (general_rewrite_ebindings lft2rgt all_occurrences (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let rewriteLR_bindings = general_rewrite_bindings true all_occurrences
-let rewriteRL_bindings = general_rewrite_bindings false all_occurrences
-
 let rewriteLR = general_rewrite true all_occurrences
 let rewriteRL = general_rewrite false all_occurrences
 
-let rewriteLRin_bindings = general_rewrite_bindings_in true all_occurrences
-let rewriteRLin_bindings = general_rewrite_bindings_in false all_occurrences
-
 let conditional_rewrite_in lft2rgt id tac (c,bl) = 
   tclTHENSFIRSTn
     (general_rewrite_ebindings_in lft2rgt all_occurrences id (c,bl) false)
     [|tclIDTAC|] (tclCOMPLETE tac)
 
-let rewriteRL_clause = function
-  | None -> rewriteRL_bindings
-  | Some id -> rewriteRLin_bindings id
-
 (* Replacing tactics *)
 
 (* eq,sym_eq : equality on Type and its symmetry theorem
@@ -973,10 +958,6 @@ let dEqThen with_evars ntac = function
 
 let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
 
-let rewrite_msg = function 
-  | None -> str "passed term is not a primitive equality" 
-  | Some id -> pr_id id ++ str "does not satisfy preconditions "
-
 let swap_equands gls eqn =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
   applist(lbeq.eq,[t;e2;e1])
@@ -986,10 +967,6 @@ let swapEquandsInConcl gls =
   let sym_equal = lbeq.sym in
   refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
 
-let swapEquandsInHyp id gls =
-  cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))
-    (tclTHEN swapEquandsInConcl) gls
-
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
@@ -1278,49 +1255,4 @@ let replace_multi_term dir_opt c  =
   in 
   rewrite_multi_assumption_cond cond_eq_fun 
 
-(* JF. old version 
-let rewrite_assumption_cond faildir gl =
-   let rec arec = function
-      | [] -> error "No such assumption."
-      | (id,_,t)::rest ->
-	  (try let dir = faildir t gl in
-	       general_rewrite dir (mkVar id) gl
-	   with Failure _ | UserError _  ->  arec rest)
-   in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
-   let rec arec = function
-      | [] -> error "No such assumption."
-      | (id,_,t)::rest ->
-	  (try let dir = faildir t gl in
-	       general_rewrite_in dir hyp (mkVar id) gl
-	   with Failure _ | UserError _ ->  arec rest)
-   in arec (pf_hyps gl)
-
-let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
-
-let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
-   
-let replace_term t = rewrite_assumption_cond (cond_eq_term t)
-   
-let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
-
-let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
-   
-let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
-*)
-
-let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
-
-let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
-
-let replace_term t = replace_multi_term None t Tacticals.onConcl
-
-let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
-
-let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
-
-let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
-
 let _ = Tactics.register_general_multi_rewrite general_multi_rewrite
diff --git a/tactics/equality.mli b/tactics/equality.mli
index df59867bb..bcbe3e222 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -32,11 +32,6 @@ val general_rewrite_bindings :
 val general_rewrite : 
   bool -> occurrences -> constr -> tactic
 
-(* Obsolete, use [general_rewrite_bindings l2r]
-[val rewriteLR_bindings       : constr with_bindings -> tactic]
-[val rewriteRL_bindings       : constr with_bindings -> tactic]
-*)
-
 (* Equivalent to [general_rewrite l2r] *)
 val rewriteLR   : constr -> tactic
 val rewriteRL   : constr  -> tactic
diff --git a/toplevel/class.ml b/toplevel/class.ml
index d2d399f10..11c5bf398 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -29,10 +29,6 @@ open Safe_typing
 
 let strength_min l = if List.mem Local l then Local else Global
 
-let id_of_varid c = match kind_of_term c with
-  | Var id -> id
-  | _ -> anomaly "class__id_of_varid"
-
 (* Errors *)
 
 type coercion_error_kind =
@@ -103,15 +99,6 @@ let uniform_cond nargs lt =
   in 
   aux (nargs,lt)
 
-let id_of_cl  = function
-  | CL_FUN -> id_of_string "FUNCLASS"
-  | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (con_label kn)
-  | CL_IND ind ->
-      let (_,mip) = Global.lookup_inductive ind in
-      mip.mind_typename
-  | CL_SECVAR id -> id
-
 let class_of_global = function
   | ConstRef sp -> CL_CONST sp
   | IndRef sp -> CL_IND sp
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index b6c664020..e5c3322a3 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -37,10 +37,6 @@ let typeclasses_db = "typeclass_instances"
 let qualid_of_con c = 
   Qualid (dummy_loc, shortest_qualid_of_global Idset.empty (ConstRef c))
 
-let set_rigid c = 
-  Auto.add_hints false [typeclasses_db] 
-    (Vernacexpr.HintsTransparency ([qualid_of_con c], false))
-
 let _ =
   Typeclasses.register_add_instance_hint 
     (fun inst pri ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6e000bc74..d07c4973e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -47,9 +47,6 @@ open Mod_subst
 open Evd
 open Decls
 
-let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
-
 let rec abstract_constr_expr c = function
   | [] -> c
   | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
@@ -73,14 +70,6 @@ let rec under_binders env f n c =
 	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
       | _ -> assert false
 
-let rec destSubCast c = match kind_of_term c with
-  | Lambda (x,t,c) -> 
-      let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
-  | LetIn (x,b,t,c) ->
-      let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
-  | Cast (b,_, u) -> (b,u)
-  | _ -> assert false
-
 let rec complete_conclusion a cs = function
   | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
   | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
@@ -288,7 +277,7 @@ let _ =
       optwrite = (fun b -> eq_flag := b) }
 
 (* boolean equality *)
-let (inScheme,outScheme) =  
+let (inScheme,_) =  
   declare_object {(default_object "EQSCHEME") with 
                     cache_function = Ind_tables.cache_scheme; 
                     load_function = (fun _ -> Ind_tables.cache_scheme); 
@@ -321,21 +310,21 @@ let declare_eq_scheme sp =
 (* decidability of eq *)
 
 
-let (inBoolLeib,outBoolLeib) =
+let (inBoolLeib,_) =
   declare_object {(default_object "BOOLLIEB") with
                     cache_function = Ind_tables.cache_bl;
                     load_function = (fun _ -> Ind_tables.cache_bl);
                     subst_function = Auto_ind_decl.subst_in_constr;
                     export_function = Ind_tables.export_bool_leib }
 
-let (inLeibBool,outLeibBool) =
+let (inLeibBool,_) =
   declare_object {(default_object "LIEBBOOL") with
                     cache_function = Ind_tables.cache_lb;
                     load_function = (fun _ -> Ind_tables.cache_lb);
                     subst_function = Auto_ind_decl.subst_in_constr;
                     export_function = Ind_tables.export_leib_bool }
 
-let (inDec,outDec) =
+let (inDec,_) =
   declare_object {(default_object "EQDEC") with
                     cache_function = Ind_tables.cache_dec;
                     load_function = (fun _ -> Ind_tables.cache_dec);
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e736fc676..729db2d02 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -51,9 +51,6 @@ let load_rcfile() =
   else 
     Flags.if_verbose msgnl (str"Skipping rcfile loading.")
 
-let add_ml_include s =
-  Mltop.add_ml_dir s
-
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path d s =
   Mltop.add_path d (Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
@@ -64,11 +61,6 @@ let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
-(* Because find puts "./" and the loadpath is not nicely pretty-printed *)
-let hm2 s = 
-  let n = String.length s in
-  if n > 1 && s.[0] = '.' && s.[1] = '/' then String.sub s 2 (n-2) else s
-
 (* The list of all theories in the standard library /!\ order does matter *)
 let theories_dirs_map = [
     "theories/Unicode", "Unicode" ;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index cd13c6c88..da63382bf 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -72,7 +72,6 @@ let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
 let set_include d p =
   let p = dirpath_of_string p in
   Library.check_coq_overwriting p;