Remove some unused values and types

5 files changed, 0 insertions, 18 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..35cfe8b542 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -52,8 +52,6 @@ let replace_in_clause_maybe_by ist c1 c2 cl tac =
 let replace_term ist dir_opt c cl =
   with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
 
-let clause = Pltac.clause_dft_concl
-
 TACTIC EXTEND replace
    ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
 -> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index bcb28f77ce..a853576f25 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -136,7 +136,6 @@ let feedback_results results =
 let format_sec x = (Printf.sprintf "%.3fs" x)
 let format_ratio x = (Printf.sprintf "%.1f%%" (100. *. x))
 let padl n s = ws (max 0 (n - utf8_length s)) ++ str s
-let padr n s = str s ++ ws (max 0 (n - utf8_length s))
 let padr_with c n s =
   let ulength = utf8_length s in
   str (utf8_sub s 0 n) ++ str (String.make (max 0 (n - ulength)) c)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8cda73b4bf..ef1d69d35b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -88,9 +88,6 @@ let rec parse_user_entry s sep =
   else
     Uentry s
 
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
 let interp_entry_name interp symb =
   let rec eval = function
   | Ulist1 e -> Ulist1 (eval e)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e9..75227def0f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function
       GRef (loc,locate_global_with_alias lqid,None), 
 	if strict then None else Some (CRef (r,None))
 
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e9..fcdf7bb2cd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -436,12 +436,6 @@ let interp_hyp_list_as_list ist env sigma (loc,id as x) =
 let interp_hyp_list ist env sigma l =
   List.flatten (List.map (interp_hyp_list_as_list ist env sigma) l)
 
-let interp_move_location ist env sigma = function
-  | MoveAfter id -> MoveAfter (interp_hyp ist env sigma id)
-  | MoveBefore id -> MoveBefore (interp_hyp ist env sigma id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar (loc, id) ->