Remove some unused values and types

11 files changed, 0 insertions, 133 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8dae17d69..df81bc78c 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -19,12 +19,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-let local_assum (na, t) =
-  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
-  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
 (* let msgnl = Pp.msgnl *)
 
 (*
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb759..35cfe8b54 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 bcb28f77c..a853576f2 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 8cda73b4b..ef1d69d35 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 3f83f104e..75227def0 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 50f43931e..fcdf7bb2c 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) ->
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b1ff59e78..41f2edfcf 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -153,7 +153,6 @@ module Make (P:Polynom.S) = struct
   type coef = P.t
   let coef0 = P.of_num (Num.Int 0)
   let coef1 = P.of_num (Num.Int 1)
-  let coefm1 = P.of_num (Num.Int (-1))
   let string_of_coef c = "["^(P.to_string c)^"]"
 
 (***********************************************************************
@@ -252,59 +251,6 @@ let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
   in 
   (stringP p true)
 
-
-
-let print_pol zeroP hdP tlP coefterm monterm string_of_coef
-    dimmon string_of_exp lvar p =
-
-  let rec print_mon m coefone =
-    let s=ref [] in
-    for i=1 to (dimmon m) do
-      (match (string_of_exp m i) with
-        "0" -> ()
-      | "1" -> s:= (!s) @ [(getvar lvar (i-1))]
-      | e -> s:= (!s) @ [((getvar lvar (i-1)) ^ "^" ^ e)]);
-    done;
-    (match !s with
-      [] -> if coefone 
-      then print_string "1"
-      else ()
-    | l -> if coefone 
-    then print_string (String.concat "*" l)
-    else (print_string "*"; 
-          print_string (String.concat "*" l)))
-  and print_term t start = let a = coefterm t and m = monterm t in
-  match (string_of_coef a) with
-    "0" -> ()
-  | "1" ->(match start with
-      true -> print_mon m true
-    |false -> (print_string "+ ";
-               print_mon m true))
-  | "-1" ->(print_string "-";print_space();print_mon m true)
-  | c -> if (String.get c 0)='-'
-  then (print_string "- ";
-        print_string (String.sub c 1 
-                        ((String.length c)-1));
-        print_mon m false)
-  else (match start with
-    true -> (print_string c;print_mon m false)
-  |false -> (print_string "+ ";
-             print_string c;print_mon m false))
-  and printP p start = 
-    if (zeroP p)
-    then (if start 
-    then print_string("0")
-    else ())
-    else (print_term (hdP p) start;
-          if start then open_hovbox 0;
-          print_space();
-          print_cut();
-          printP (tlP p) false)
-  in open_hovbox 3;
-  printP p true;
-  print_flush()
-
-
 let stringP metadata (p : poly) =
   string_of_pol 
     (fun p -> match p with [] -> true | _ -> false)
@@ -595,9 +541,6 @@ let addS x l =    l @ [x] (* oblige de mettre en queue sinon le certificat decon
  critical pairs/s-polynomials
  *)
 
-let ordcpair ((i1,j1),m1) ((i2,j2),m2) =
-  compare_mon m1 m2 
-
 module CPair =
 struct
 type t = (int * int) * Monomial.t
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index a5b016611..632b9dac1 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -22,7 +22,6 @@ open Utile
 let num_0 = Int 0
 and num_1 = Int 1
 and num_2 = Int 2
-and num_10 = Int 10
 
 let numdom r =
   let r' = Ratio.normalize_ratio (ratio_of_num r) in
@@ -35,7 +34,6 @@ module BigInt = struct
   type t = big_int
   let of_int = big_int_of_int
   let coef0 = of_int 0
-  let coef1 = of_int 1
   let of_num = Num.big_int_of_num
   let to_num = Num.num_of_big_int
   let equal = eq_big_int
@@ -49,7 +47,6 @@ module BigInt = struct
   let div = div_big_int
   let modulo = mod_big_int
   let to_string = string_of_big_int
-  let to_int x = int_of_big_int x
   let hash x =
     try (int_of_big_int x)
     with Failure _ -> 1
@@ -61,15 +58,6 @@ module BigInt = struct
     then a
     else if lt a b then pgcd b a else pgcd b (modulo a b)
 
-
-  (* signe du pgcd = signe(a)*signe(b) si non nuls. *)
-  let pgcd2 a b =
-    if equal a coef0 then b
-    else if equal b coef0 then a
-    else let c = pgcd (abs a) (abs b) in
-    if ((lt coef0 a)&&(lt b coef0))
-      ||((lt coef0 b)&&(lt a coef0))
-    then opp c else c
 end
 
 (*
@@ -146,8 +134,6 @@ let mul = function
   | (Const n,q) when eq_num n num_1 -> q
   | (p,q) -> Mul(p,q)
 
-let unconstr = mkRel 1
-
 let tpexpr =
   lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PExpr")
 let ttconst = lazy (gen_constant "CC" ["setoid_ring";"Ring_polynom"] "PEc")
@@ -271,20 +257,6 @@ let set_nvars_term nvars t =
     | Pow (t1,n) ->  aux t1 nvars
   in aux t nvars
 
-let string_of_term p =
-  let rec aux p =
-    match p with
-    | Zero -> "0"
-    | Const r -> string_of_num r
-    | Var v -> "x"^v
-    | Opp t1 -> "(-"^(aux t1)^")"
-    | Add (t1,t2) -> "("^(aux t1)^"+"^(aux t2)^")"
-    | Sub (t1,t2) ->  "("^(aux t1)^"-"^(aux t2)^")"
-    | Mul (t1,t2) ->  "("^(aux t1)^"*"^(aux t2)^")"
-    | Pow (t1,n) ->  (aux t1)^"^"^(string_of_int n)
-  in aux p
-
-
 (***********************************************************************
    Coefficients: recursive polynomials
  *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index dd68eac24..6e072e831 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -279,8 +279,6 @@ let my_constant c =
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
-let new_ring_path =
-  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc7963b2d..60c199bf5 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -90,8 +90,6 @@ let pp s = !pp_ref s
 let env_size env = List.length (Environ.named_context env)
 let safeDestApp c =
   match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |]
-let get_index = function ArgArg i -> i | _ ->
-  CErrors.anomaly (str"Uninterpreted index")
 (* Toplevel constr must be globalized twice ! *)
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -304,8 +302,6 @@ let unif_EQ_args env sigma pa a =
 
 let unif_HO env ise p c = Evarconv.the_conv_x env p c ise
 
-let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise
-
 let unif_HO_args env ise0 pa i ca =
   let n = Array.length pa in
   let rec loop ise j =
@@ -371,11 +367,6 @@ let unif_end env sigma0 ise0 pt ok =
     let s, uc', t = nf_open_term sigma0 ise2 t in
     s, Evd.union_evar_universe_context uc uc', t
 
-let pf_unif_HO gl sigma pt p c =
-  let env = pf_env gl in
-  let ise = unif_HO env (create_evar_defs sigma) p c in
-  unif_end env (project gl) ise pt (fun _ -> true)
-
 let unify_HO env sigma0 t1 t2 =
   let sigma = unif_HO env sigma0 t1 t2 in
   let sigma, uc, _ = unif_end env sigma0 sigma t2 (fun _ -> true) in
@@ -440,10 +431,6 @@ let all_ok _ _ = true
 let proj_nparams c =
   try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0
 
-let isFixed c = match kind_of_term c with
-  | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true
-  | _ -> false
-
 let isRigid c = match kind_of_term c with
   | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
   | _ -> false
@@ -917,13 +904,6 @@ let pp_pattern (sigma, p) =
 let pr_cpattern = pr_term
 let pr_rpattern _ _ _ = pr_pattern
 
-let pr_option f = function None -> mt() | Some x -> f x
-let pr_ssrpattern _ _ _ = pr_option pr_pattern
-let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]")
-let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep
-let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")")
-let pr_ssrpattern_roundp  _ _ _ = pr_pattern_roundp
-
 let wit_rpatternty = add_genarg "rpatternty" pr_pattern
 
 let glob_ssrterm gs = function
@@ -1045,7 +1025,6 @@ let interp_wit wit ist gl x =
   let arg = interp_genarg ist globarg in
   let (sigma, arg) = of_ftactic arg gl in
   sigma, Value.cast (topwit wit) arg
-let interp_constr = interp_wit wit_constr
 let interp_open_constr ist gl gc =
   interp_wit wit_open_constr ist gl gc
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 894cdb943..1f984b160 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -226,7 +226,6 @@ val loc_of_cpattern : cpattern -> Loc.t
 val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
-val cpattern_of_id : Names.variable -> cpattern
 val pr_constr_pat : constr -> Pp.std_ppcmds
 val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma
 val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma