Removing dead code.

5 files changed, 3 insertions, 36 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 5ba93eda0..61042ccc1 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -306,8 +306,6 @@ let init () =
 
 type emitcodes = string
 
-let copy = String.copy
-
 let length = String.length
 
 type to_patch = emitcodes * (patch list) * fv
@@ -332,8 +330,6 @@ let subst_patch s (ri,pos) =
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
-let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
-
 type body_code =
   | BCdefined of to_patch
   | BCalias of Names.constant
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 632b4daea..d0df5c7b3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -151,7 +151,7 @@ let remember_subst u subst =
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env =
+let make_subst env =
   let rec make subst = function
     | (_,Some _,_)::sign, exp, args ->
         make subst (sign, exp, args)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9e8ffbc7f..925b2248d 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -139,7 +139,6 @@ let rec repr g u =
     | Equiv v -> repr g v
     | Canonical arc -> arc
 
-let get_prop_arc g = repr g Level.prop
 let get_set_arc g = repr g Level.set
 let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
@@ -155,7 +154,7 @@ let use_index g u =
 
 (* [safe_repr] is like [repr] but if the graph doesn't contain the
    searched universe, we add it. *)
-let rec safe_repr g u =
+let safe_repr g u =
   let rec safe_repr_rec entries u =
     match UMap.find u entries with
     | Equiv v -> safe_repr_rec entries v
@@ -745,9 +744,6 @@ let check_constraints c g =
 
 (* Normalization *)
 
-let lookup_level u g =
-  try Some (UMap.find u g) with Not_found -> None
-
 (** [normalize_universes g] returns a graph where all edges point
     directly to the canonical representent of their target. The output
     graph should be equivalent to the input graph from a logical point
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ecce4a0ff..23de87d7d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -97,7 +97,6 @@ let intern_or_var f ist = function
   | ArgArg x -> ArgArg (f x)
 
 let intern_int_or_var = intern_or_var (fun (n : int) -> n)
-let intern_id_or_var = intern_or_var (fun (id : Id.t) -> id)
 let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
 let intern_global_reference ist = function
@@ -339,7 +338,7 @@ let intern_typed_pattern ist p =
   (* type it, so we remember the pattern as a glob_constr only *)
   (intern_constr_gen true false ist p,dummy_pat)
 
-let rec intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
+let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
   let interp_ref r =
     try Inl (intern_evaluable ist r)
     with e when Logic.catchable_exception e ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 16cafafeb..a0fa9b5f3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -363,10 +363,6 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
   try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id)
   with Not_found -> IntroIdentifier id
 
-let interp_hint_base ist s =
-  try try_interp_ltac_var coerce_to_hint_base ist None (dloc,Id.of_string s)
-  with Not_found -> s
-
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
@@ -685,10 +681,6 @@ let interp_constr_list ist env sigma c =
 let interp_open_constr_list =
   interp_constr_in_compound_list (fun x -> x) (fun x -> x) interp_open_constr
 
-let interp_auto_lemmas ist env sigma lems =
-  let local_sigma, lems = interp_open_constr_list ist env sigma lems in
-  List.map (fun lem -> (local_sigma,lem)) lems
-
 (* Interprets a type expression *)
 let pf_interp_type ist gl =
   interp_type ist (pf_env gl) (project gl)
@@ -864,11 +856,6 @@ let interp_message ist l =
   Ftactic.List.map (interp_message_token ist) l >>= fun l ->
   Ftactic.return (prlist_with_sep spc (fun x -> x) l)
 
-let interp_message ist l =
-  let open Ftactic in
-  Ftactic.List.map (interp_message_token ist) l >>= fun l ->
-  Ftactic.return (prlist_with_sep spc (fun x -> x) l)
-
 let rec interp_intro_pattern ist env sigma = function
   | loc, IntroAction pat ->
       let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
@@ -977,19 +964,11 @@ let interp_constr_with_bindings ist env sigma (c,bl) =
   let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c,bl)
 
-let interp_constr_with_bindings_arg ist env sigma (keep,c) =
-  let sigma, c = interp_constr_with_bindings ist env sigma c in
-  sigma, (keep,c)
-
 let interp_open_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
   let sigma, c = interp_open_constr ist env sigma c in
   sigma, (c, bl)
 
-let interp_open_constr_with_bindings_arg ist env sigma (keep,c) =
-  let sigma, c = interp_open_constr_with_bindings ist env sigma c in
-  sigma,(keep,c)
-
 let loc_of_bindings = function
 | NoBindings -> Loc.ghost
 | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
@@ -1128,9 +1107,6 @@ let mk_open_constr_value ist gl c =
   sigma, Value.of_constr c_interp
 let mk_hyp_value ist env sigma c =
   (mkVar (interp_hyp ist env sigma c))
-let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c)
-
-let pack_sigma (sigma,c) = {it=c;sigma=sigma;}
 
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t =