Removing dead code.

2 files changed, 1 insertions, 26 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ecce4a0ff3..23de87d7db 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 16cafafeb8..a0fa9b5f3e 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 =