Removing dead code.

4 files changed, 1 insertions, 62 deletions

diff --git a/library/heads.ml b/library/heads.ml
index fa0393019..31908816b 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
 open Term
@@ -14,7 +13,6 @@ open Vars
 open Mod_subst
 open Environ
 open Globnames
-open Nameops
 open Libobject
 open Lib
 
@@ -186,15 +184,3 @@ let inHead : head_obj -> obj =
 let declare_head c =
   let hd = compute_head c in
   add_anonymous_leaf (inHead (c,hd))
-
-(** Printing *)
-
-let pr_head = function
-| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst
-| RigidHead (RigidType) -> str "rigid type"
-| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id
-| ConstructorHead -> str "constructor"
-| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt())
-| NotImmediatelyComputableHead -> str "unknown"
-
-
diff --git a/library/impargs.ml b/library/impargs.ml
index c7faff33c..0126c4ad7 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -14,7 +14,6 @@ open Term
 open Reduction
 open Declarations
 open Environ
-open Inductive
 open Libobject
 open Lib
 open Pp
diff --git a/library/lib.ml b/library/lib.ml
index 31f983595..10b4915a2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -446,10 +446,6 @@ let section_segment_of_constant con =
 let section_segment_of_mutual_inductive kn =
   Names.Mindmap.find kn (snd (pi3 (List.hd !sectab)))
 
-let rec list_mem_assoc x = function
-  | [] -> raise Not_found
-  | (a, _) :: l -> Names.Id.equal a x || list_mem_assoc x l
-
 let section_instance = function
   | VarRef id ->
       if List.exists (fun (id',_,_,_) -> Names.id_eq id id') 
diff --git a/library/universes.ml b/library/universes.ml
index 9c8d8a512..be49294a2 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -10,9 +10,7 @@ open Util
 open Pp
 open Names
 open Term
-open Context
 open Environ
-open Locus
 open Univ
 
 type universe_constraint_type = ULe | UEq | ULub
@@ -471,12 +469,8 @@ let add_list_map u t map =
       match rm with Some t -> rm | None -> None) l r
   in LMap.add u d' lr
 
-let find_list_map u map =
-  try LMap.find u map with Not_found -> []
-
 module UF = LevelUnionFind
-type universe_full_subst = (universe_level * universe) list
-  
+
 (** Precondition: flexible <= ctx *)
 let choose_canonical ctx flexible algs s =
   let global = LSet.diff s ctx in
@@ -499,8 +493,6 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
-open Universe
-
 let subst_puniverses subst (c, u as cu) =
   let u' = Instance.subst subst u in
     if u' == u then cu else (c, u')
@@ -531,9 +523,6 @@ let subst_univs_fn_puniverses lsubst (c, u as cu) =
   let u' = Instance.subst_fn lsubst u in
     if u' == u then cu else (c, u')
 
-let subst_univs_puniverses subst cu =
-  subst_univs_fn_puniverses (Univ.level_subst_of (Univ.make_subst subst)) cu
-
 let nf_evars_and_universes_gen f subst =
   let lsubst = Univ.level_subst_of subst in
   let rec aux c =
@@ -557,16 +546,10 @@ let nf_evars_and_universes_gen f subst =
     | _ -> map_constr aux c
   in aux
 
-let nf_evars_and_universes_subst f subst =
-  nf_evars_and_universes_gen f (Univ.make_subst subst)
-
 let nf_evars_and_universes_opt_subst f subst =
   let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in
     nf_evars_and_universes_gen f subst
 
-let subst_univs_full_constr subst c = 
-  nf_evars_and_universes_subst (fun _ -> None) subst c
-
 let fresh_universe_context_set_instance ctx =
   if ContextSet.is_empty ctx then LMap.empty, ctx
   else
@@ -652,16 +635,6 @@ let pr_universe_body = function
 
 let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
 
-let is_defined_var u l = 
-  try
-    match LMap.find u l with
-    | Some _ -> true
-    | None -> false
-  with Not_found -> false
-
-let subst_univs_subst u l s = 
-  LMap.add u l s
-    
 exception Found of Level.t
 let find_inst insts v =
   try LMap.iter (fun k (enf,alg,v') ->
@@ -669,13 +642,6 @@ let find_inst insts v =
 	insts; raise Not_found
   with Found l -> l
 
-let add_inst u (enf,b,lbound) insts =
-  match lbound with
-  | Some v -> LMap.add u (enf,b,v) insts
-  | None -> insts
-
-exception Stays
-
 let compute_lbound left =
  (** The universe variable was not fixed yet.
      Compute its level using its lower bound. *)
@@ -693,11 +659,6 @@ let compute_lbound left =
 	 else None))
       None left
   
-let maybe_enforce_leq lbound u cstrs = 
-  match lbound with
-  | Some lbound -> enforce_leq lbound (Universe.make u) cstrs
-  | None -> cstrs
-
 let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
   if enforce then
     let inst = Universe.make u in
@@ -941,9 +902,6 @@ let simplify_universe_context (univs,csts) =
 let is_small_leq (l,d,r) =
   Level.is_small l && d == Univ.Le
 
-let is_prop_leq (l,d,r) =
-  Level.equal Level.prop l && d == Univ.Le
-
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
   if Level.equal Level.prop l && d == Univ.Lt then