Removing dead code.

53 files changed, 12 insertions, 615 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 841a89584..93feb8b46 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -28,7 +28,6 @@ open Topconstr
 open Nametab
 open Notation
 open Inductiveops
-open Misctypes
 open Decl_kinds
 
 (** constr_expr -> glob_constr translation:
@@ -298,12 +297,6 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
-let set_scope env = function
-  | CastConv (GSort _) -> set_type_scope env
-  | CastConv (GRef (_,ref,_) | GApp (_,GRef (_,ref,_),_)) ->
-      {env with tmp_scope = compute_scope_of_global ref}
-  | _ -> env
-
 let rec it_mkGProd loc2 env body =
   match env with
       (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
@@ -1299,18 +1292,6 @@ let merge_impargs l args =
       | _ -> a::l)
     l args
 
-let check_projection isproj nargs r =
-  match (r,isproj) with
-  | GRef (loc, ref, _), Some _ ->
-      (try
-	if not (Int.equal nargs 1) then
-	  user_err_loc (loc,"",str "Projection does not have the right number of explicit parameters.");
-      with Not_found ->
-	user_err_loc
-	(loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection."))
-  | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.")
-  | _, None -> ()
-
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
@@ -1360,10 +1341,6 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let is_projection_ref env = function
-  | ConstRef c -> Environ.is_projection c env
-  | _ -> false
-
 let internalize globalenv env allow_patvar lvar c =
   let rec intern env = function
     | CRef (ref,us) as x ->
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 3df071aff..6c4d76340 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -99,10 +99,6 @@ let init_constant dir s =
   let d = "Init"::dir in
   check_required_library (coq::d); gen_constant "Coqlib" d s
 
-let logic_constant dir s =
-  let d = "Logic"::dir in
-  check_required_library (coq::d); gen_constant "Coqlib" d s
-
 let logic_reference dir s =
   let d = "Logic"::dir in
   check_required_library ("Coq"::d); gen_reference "Coqlib" d s
@@ -139,9 +135,6 @@ let logic_type_module = make_dir logic_type_module_name
 let datatypes_module_name = init_dir@["Datatypes"]
 let datatypes_module = make_dir datatypes_module_name
 
-let arith_module_name = arith_dir@["Arith"]
-let arith_module = make_dir arith_module_name
-
 let jmeq_module_name = [coq;"Logic";"JMeq"]
 let jmeq_module = make_dir jmeq_module_name
 
@@ -273,9 +266,6 @@ let build_coq_eq_data () =
   trans = Lazy.force coq_eq_trans;
   congr = Lazy.force coq_eq_congr }
 
-let make_dirpath dir = 
-  Names.make_dirpath (List.map id_of_string dir)
-
 let build_coq_eq () = Lazy.force coq_eq_eq
 let build_coq_eq_refl () = Lazy.force coq_eq_refl
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
diff --git a/interp/notation.ml b/interp/notation.ml
index 6fd6001f4..ec82c8aea 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -214,18 +214,6 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 
-let compare_interp_rule x y =
-  match x, y with
-  | NotationRule (sno1, n1), NotationRule (sno2, n2) ->
-      (match sno1, sno2 with
-      | None, None -> String.compare n1 n2
-      | None, Some _ -> -1
-      | Some sn1, Some sn2 -> String.compare sn1 sn2
-      | Some _, None -> 1)
-  | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2
-  | NotationRule _, SynDefRule _ -> -1
-  | SynDefRule _, NotationRule _ -> 1
-
 (* We define keys for glob_constr and aconstr to split the syntax entries
    according to the key of the pattern (adapted from Chet Murthy by HH) *)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a023462b7..524f6d743 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -82,7 +82,6 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let pr_global r = pr_global_env Id.Set.empty r
 let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
 
 let allow_compat_notations = ref true
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 9be04c765..b2aa5690b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -143,7 +143,6 @@ let mkApp (f, a) =
       | App (g, cl) -> App (g, Array.append cl a)
       | _ -> App (f, a)
 
-let out_punivs (a, _) = a
 let map_puniverses f (x,u) = (f x, u)
 let in_punivs a = (a, Univ.Instance.empty)
 
@@ -547,9 +546,6 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
 let rec eq_constr m n =
   (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n
 
-(** Strict equality of universe instances. *)
-let compare_constr = compare_head_gen (fun _ -> Instance.equal) Sorts.equal
-
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 let eq_constr_univs univs m n =
@@ -989,7 +985,7 @@ module Hsorts =
 	| Type u -> 2 + Universe.hash u
     end)
 
-let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
+(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
 let hcons =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5bd0edf69..48a7964c3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -220,10 +220,6 @@ let universes_and_subst_of cb u =
   let subst = Univ.make_universe_subst u univs in
     subst, Univ.instantiate_univ_context subst univs
 
-let get_regular_arity = function
-  | RegularArity a -> a
-  | TemplateArity _ -> assert false
-
 let map_regular_arity f = function
   | RegularArity a as ar -> 
     let a' = f a in 
@@ -374,8 +370,6 @@ let add_mind kn mib env =
 
 (* Lookup of section variables *)
 
-let constant_body_hyps cb = cb.const_hyps
-
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
   Context.vars_of_named_context cmap.const_hyps
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 94e4479d2..83f1e74ba 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -12,10 +12,8 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
-open Entries
 open Reduction
 open Inductive
 open Type_errors
@@ -62,7 +60,6 @@ let assumption_of_judgment env t ty =
 (* Prop and Set *)
 
 let judge_of_prop = mkSort type1_sort
-let judge_of_set = judge_of_prop
 
 let judge_of_prop_contents _ = judge_of_prop
 
@@ -122,16 +119,6 @@ let type_of_constant_knowing_parameters env cst paramtyps =
   let ty, cu = constant_type env cst in
     type_of_constant_knowing_parameters_arity env ty paramtyps, cu
 
-let type_of_constant_type env t =
-  type_of_constant_knowing_parameters_arity env t [||]
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
-  let ar = constant_type_in env cst in
-    type_of_constant_knowing_parameters_arity env ar [||]
-
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
@@ -142,18 +129,6 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args =
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
 
-let type_of_projection env (cst,u) =
-  let cb = lookup_constant cst env in
-  match cb.const_proj with
-  | Some pb -> 
-    if cb.const_polymorphic then
-      let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
-      let subst = make_inductive_subst mib u in
-	Vars.subst_univs_level_constr subst pb.proj_type
-    else pb.proj_type
-  | None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-
 (* Type of a lambda-abstraction. *)
 
 (* [judge_of_abstraction env name var j] implements the rule
@@ -169,11 +144,6 @@ let type_of_projection env (cst,u) =
 let judge_of_abstraction env name var ty =
   mkProd (name, var, ty)
 
-(* Type of let-in. *)
-
-let judge_of_letin env name defj typj j =
-  subst1 defj j
-
 (* Type of an application. *)
 
 let make_judgev c t = 
@@ -490,26 +460,3 @@ let infer_type env constr =
 let infer_v env cv =
   let jv = execute_array env cv in
     make_judgev cv jv
-
-(* Typing of several terms. *)
-
-let infer_local_decl env id = function
-  | LocalDef c ->
-      let t = execute env c in
-      (Name id, Some c, t)
-  | LocalAssum c ->
-      let t = execute env c in
-      (Name id, None, assumption_of_judgment env c t)
-
-let infer_local_decls env decls =
-  let rec inferec env = function
-  | (id, d) :: l ->
-      let (env, l) = inferec env l in
-      let d = infer_local_decl env id d in
-	(push_rel d env, add_rel_decl d l)
-  | [] -> (env, empty_rel_context) in
-  inferec env decls
-
-(* Exported typing functions *)
-
-let typing env c = infer env c
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 85d04e5e2..014bfba29 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -102,14 +102,6 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-let is_logic_type t = is_prop_sort t.utj_type
-
-(* [infos] is a sequence of pair [islogic,issmall] for each type in
-   the product of a constructor or arity *)
-
-let is_small infos = List.for_all (fun (logic,small) -> small) infos
-let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
-
 (* An inductive definition is a "unit" if it has only one constructor
    and that all arguments expected by this constructor are
    logical, this is the case for equality, conjunction of logical properties
@@ -153,23 +145,9 @@ let infos_and_sort env ctx t =
    w1,w2,w3 <= u3
 *)
 
-let extract_level (_,_,lc,(_,lev)) =
-  (* Enforce that the level is not in Prop if more than one constructor *)
-  (* if Array.length lc >= 2 then sup type0_univ lev else lev *)
-  lev
-
-let inductive_levels arities inds =
-  let cstrs_levels = Array.map extract_level inds in
-  (* Take the transitive closure of the system of constructors *)
-  (* level constraints and remove the recursive dependencies *)
-    cstrs_levels
-
 (* This (re)computes informations relevant to extraction and the sort of an
    arity or type constructor; we do not to recompute universes constraints *)
 
-let context_set_list_union =
-  List.fold_left ContextSet.union ContextSet.empty
-
 let infer_constructor_packet env_ar_par ctx params lc =
   (* type-check the constructors *)
   let jlc = List.map (infer_type env_ar_par) lc in
@@ -691,11 +669,7 @@ let used_section_variables env inds =
       Id.Set.empty inds in
   keep_hyps env ids
 
-let lift_decl n d = 
-  map_rel_declaration (lift n) d
-
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_list n m = Array.to_list (rel_vect n m)
 let rel_appvect n m = rel_vect n (List.length m)
 
 exception UndefinableExpansion
@@ -707,7 +681,7 @@ exception UndefinableExpansion
 let compute_expansion ((kn, _ as ind), u) params ctx =
   let mp, dp, l = repr_mind kn in
   let make_proj id = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
-  let rec projections acc (na, b, t) =
+  let projections acc (na, b, t) =
     match b with
     | Some c -> acc
     | None -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f07217ac0..64b2c76f9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -19,9 +19,6 @@ open Environ
 open Reduction
 open Type_errors
 
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
-
 type mind_specif = mutual_inductive_body * one_inductive_body
 
 (* raise Not_found if not an inductive type *)
@@ -157,10 +154,6 @@ let sort_as_univ = function
 let cons_subst u su subst =
   Univ.LMap.add u su subst
 
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
 let rec make_subst env = function
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a6e107d3f..1e6f157ab 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -172,7 +172,6 @@ type conv_pb =
   | CUMUL
 
 let is_cumul = function CUMUL -> true | CONV -> false
-let is_pos = function Pos -> true | Null -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
@@ -186,8 +185,6 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
-type conv_universes = Univ.universes * Univ.constraints option
-
 let sort_cmp_universes pb s0 s1 (u, check) =
   (check.compare pb s0 s1 u, check)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3e11ede0e..0578d35fc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -802,12 +802,6 @@ let register field value by_clause senv =
       Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge
   }
 
-(* spiwack : currently unused *)
-let unregister field senv =
-  (*spiwack: todo: do things properly or delete *)
-  { senv with env = Environ.unregister senv.env field}
-(* /spiwack *)
-
 (* This function serves only for inlining constants in native compiler for now,
 but it is meant to become a replacement for environ.register *)
 let register_inline kn senv =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 147fe8a9d..437f7b832 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,10 +24,6 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let debug = true
-let prerr_endline =
-  if debug then prerr_endline else fun _ -> ()
-
 let constrain_type env j poly = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
@@ -46,15 +42,6 @@ let constrain_type env j poly = function
 
 let map_option_typ = function None -> `None | Some x -> `Some x
 
-let local_constrain_type env j = function
-  | None ->
-      j.uj_type
-  | Some t ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-      assert (eq_constr t tj.utj_val);
-      t
-
 (* Insertion of constants and parameters in environment. *)
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
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
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4e1806f5a..6177f22f3 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Names
 open Term
 open Ccalgo
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2de0fe717..73c050bb2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -468,8 +468,6 @@ let congruence_tac depth l =
    might be slow now, let's rather do something equivalent
    to a "simple apply refl_equal" *)
 
-let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal)
-
 (* The [f_equal] tactic.
 
    It mimics the use of lemmas [f_equal], [f_equal2], etc.
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 11b120c41..076107450 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Reductionops
 open Formula
 open Sequent
 open Names
-open Globnames
 open Misctypes
 
 let compare_instance inst1 inst2=
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f4a062732..8c3033d0c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -17,19 +17,6 @@ open Misctypes
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
 
-let pr_elim_scheme el =
-  let env = Global.env () in
-  let msg = str "params := " ++ Printer.pr_rel_context env el.params in
-  let env = Environ.push_rel_context el.params env in
-  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
-  let env = Environ.push_rel_context el.predicates env in
-  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
-  let env = Environ.push_rel_context el.branches env in
-  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
-  let env = Environ.push_rel_context el.args env in
-  msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
-
-
 let observe s =
   if do_observe ()
   then Pp.msg_debug s
@@ -270,10 +257,6 @@ let change_property_sort toSort princ princName =
     )
     princ_info.params
 
-
-let pp_dur time time' =
-  str (string_of_float (System.time_difference time time'))
-
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d8f006f51..961266c9c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,7 +10,6 @@ open Term
 open Vars
 open Namegen
 open Environ
-open Declareops
 open Entries
 open Pp
 open Names
@@ -125,7 +124,6 @@ let lt = function () -> (coq_base_constant "lt")
 let le = function () -> (coq_base_constant "le")
 let ex = function () -> (coq_base_constant "ex")
 let nat = function () -> (coq_base_constant "nat")
-let coq_sig = function () -> (coq_base_constant "sig")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> error "module Recdef not loaded"
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1c9796b4d..d93574b47 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -687,7 +687,7 @@ and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),
 	 (fst (decompose_app_vect (substl ks h'))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
-and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
+(*and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (exp,projs) when Array.length projs > 0 -> 
@@ -703,7 +703,7 @@ and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
 		   (Stack.append_app_list sk2 Stack.empty)
 	     else raise (Failure "")
 	 with Failure _ -> UnifFailure(evd,NotSameHead))
-    | _ -> UnifFailure (evd,NotSameHead)
+    | _ -> UnifFailure (evd,NotSameHead)*)
 
 (* Profiling *)
 let evar_conv_x =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 7222085e1..66d65bab6 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Util
-open Pp
 open Errors
 open Names
 open Term
@@ -1194,9 +1193,6 @@ exception NotEnoughInformationEvarEvar of constr
 exception OccurCheckIn of evar_map * constr
 exception MetaOccurInBodyInternal
 
-let fast_stats = ref 0
-let not_fast_stats = ref 0
-
 let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
   let aliases = make_alias_map env in
   let evdref = ref evd in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0a9b37698..a842134df 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -126,10 +126,6 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_flexible_level evd l =
-  let a = Univ.Instance.to_array l in
-    Array.exists (fun l -> Evd.is_flexible_level evd l) a
-    
 let has_undefined_evars or_sorts evd t =
   let rec has_ev t =
     match kind_of_term t with
@@ -833,35 +829,6 @@ let get_template_constructor_type evdref (ind, i) n =
   let ty = oib.mind_user_lc.(pred i) in
   let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
   let ty = substl subst ty in
-  let rec aux l ty n =
-    match l, kind_of_term ty with
-    | None :: l, Prod (na, t, t') ->
-      mkProd (na, t, aux l t' (pred n))
-    | Some u :: l, Prod (na, t, t') ->
-      let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in
-	(* evdref := set_leq_sort !evdref u'l (Type u); *)
-	let s = Univ.LMap.add u
-	  (Option.get (Univ.Universe.level u')) Univ.LMap.empty in
-	let dom = subst_univs_level_constr s t in
-	(* let codom = subst_univs_level_constr s t' in *)
-	  mkProd (na, dom, aux l t' (pred n))
-    | l, LetIn (na, t, b, t') ->
-      mkLetIn (na, t, b, aux l t' n)
-    | _ :: _, _ -> assert false (* All params should be abstracted by a forall or a let-in *)
-    | [], _ -> ty
-  in aux ar.template_param_levels ty n
-
-
-let get_template_constructor_type evdref (ind, i) n =
-  let mib,oib = Global.lookup_inductive ind in
-  let ar =
-    match oib.mind_arity with
-    | RegularArity _ -> assert false
-    | TemplateArity templ -> templ
-  in
-  let ty = oib.mind_user_lc.(pred i) in
-  let subst = Inductive.ind_subst (fst ind) mib Univ.Instance.empty in
-  let ty = substl subst ty in
     ar.template_param_levels, ty
 
 let get_template_inductive_type evdref ind n =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e36e16c05..53d1a8a0e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -954,8 +954,6 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = d.universes.uctx_local
 
-let universes evd = evd.universes.uctx_universes
-
 let universe_context evd =
   Univ.ContextSet.to_context evd.universes.uctx_local
 
@@ -1088,35 +1086,11 @@ let is_eq_sort s1 s2 =
       if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
-let is_univ_var_or_set u = 
-  not (Option.is_empty (Univ.universe_level u))
-
-type universe_global = 
-  | LocalUniv of Univ.universe_level
-  | GlobalUniv of Univ.universe_level
-
-type universe_kind = 
-  | Algebraic of Univ.universe
-  | Variable of universe_global * bool
-
-let is_univ_level_var (us, cst) algs u =
-  match Univ.universe_level u with
-  | Some l -> 
-    let glob = if Univ.LSet.mem l us then LocalUniv l else GlobalUniv l in
-      Variable (glob, Univ.LSet.mem l algs)
-  | None -> Algebraic u
-
 let normalize_universe evd =
   let vars = ref evd.universes.uctx_univ_variables in
   let normalize = Universes.normalize_universe_opt_subst vars in
     normalize
 
-let memo_normalize_universe evd =
-  let vars = ref evd.universes.uctx_univ_variables in
-  let normalize = Universes.normalize_universe_opt_subst vars in
-    (fun () -> {evd with universes = {evd.universes with uctx_univ_variables = !vars}}),
-    normalize
-
 let normalize_universe_instance evd l =
   let vars = ref evd.universes.uctx_univ_variables in
   let normalize = Univ.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in
@@ -1178,9 +1152,6 @@ let check_leq evd s s' =
 let subst_univs_context_with_def def usubst (ctx, cst) =
   (Univ.LSet.diff ctx def, Univ.subst_univs_constraints usubst cst)
 
-let subst_univs_context usubst ctx =
-  subst_univs_context_with_def (Univ.LMap.universes usubst) (Univ.make_subst usubst) ctx
-
 let normalize_evar_universe_context_variables uctx =
   let normalized_variables, undef, def, subst = 
     Universes.normalize_univ_variables uctx.uctx_univ_variables 
@@ -1195,14 +1166,6 @@ let normalize_evar_universe_context_variables uctx =
 (* let normalize_evar_universe_context_variables = *)
 (*   Profile.profile1 normvarsconstrkey normalize_evar_universe_context_variables;; *)
     
-let mark_undefs_as_rigid uctx =
-  let vars' = 
-    Univ.LMap.fold (fun u v acc ->
-      if v == None && not (Univ.LSet.mem u uctx.uctx_univ_algebraic) 
-      then acc else Univ.LMap.add u v acc)
-    uctx.uctx_univ_variables Univ.LMap.empty
-  in { uctx with uctx_univ_variables = vars' }
-
 let mark_undefs_as_nonalg uctx =
   let vars' = 
     Univ.LMap.fold (fun u v acc ->
@@ -1239,16 +1202,6 @@ let refresh_undefined_universes evd =
   let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
     evd', subst
 
-let constraints_universes c = 
-  Univ.Constraint.fold (fun (l',d,r') acc -> Univ.LSet.add l' (Univ.LSet.add r' acc))
-    c Univ.LSet.empty
-
-let is_undefined_universe_variable l vars =
-  try (match Univ.LMap.find l vars with
-      | Some u -> false
-      | None -> true)
-  with Not_found -> false
-    
 let normalize_evar_universe_context uctx = 
   let rec fixpoint uctx = 
     let ((vars',algs'), us') = 
@@ -1275,10 +1228,6 @@ let nf_univ_variables evd =
   let evd' = {evd with universes = uctx'} in
     evd', subst
 
-let normalize_univ_level fullsubst u =
-  try Univ.LMap.find u fullsubst
-  with Not_found -> Univ.Universe.make u
-  
 let nf_constraints evd =
   let subst, uctx' = normalize_evar_universe_context_variables evd.universes in
   let uctx' = normalize_evar_universe_context uctx' in
@@ -1299,7 +1248,6 @@ let add_universe_name evd s l =
     {evd with universes = {evd.universes with uctx_names = names'}}
 
 let universes evd = evd.universes.uctx_universes
-let constraints evd = evd.universes.uctx_universes
 
 (* Conversion w.r.t. an evar map and its local universes. *)
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 43552ef54..21395af02 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Context
 open Termops
-open Namegen
 open Declarations
 open Declareops
 open Environ
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 6c490d7b9..8b9e6e633 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -38,7 +38,6 @@ let default_type_ident = Id.of_string default_type_string
 let default_non_dependent_string = "H"
 let default_non_dependent_ident = Id.of_string default_non_dependent_string
 
-let default_dependent_string = "x"
 let default_dependent_ident = Id.of_string "x"
 
 (**********************************************************************)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5ae49e563..91b851d12 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -288,16 +288,6 @@ let pretype_global rigid env evd gr us =
   in
     Evd.fresh_global ~rigid ?names:instance env evd gr
 
-let is_template_polymorphic_constructor env c =
-  match kind_of_term c with
-  | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env
-  | _ -> false
-
-let is_template_polymorphic_constructor env c =
-  match kind_of_term c with
-  | Construct ((ind, i), u) -> Environ.template_polymorphic_ind ind env
-  | _ -> false
-
 let pretype_ref loc evdref env ref us =
   match ref with
   | VarRef id ->
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 7250217d6..35ac90de5 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -145,14 +145,6 @@ type cs_pattern =
   | Sort_cs of sorts_family
   | Default_cs
 
-let eq_obj_typ o1 o2 =
-  Constr.equal o1.o_DEF o2.o_DEF &&
-  Int.equal o1.o_INJ o2.o_INJ &&
-  List.equal Constr.equal o1.o_TABS o2.o_TABS &&
-  List.equal Constr.equal o1.o_TPARAMS o2.o_TPARAMS &&
-  Int.equal o1.o_NPARAMS o2.o_NPARAMS &&
-  List.equal Constr.equal o1.o_TCOMPS o2.o_TCOMPS
-
 let eq_cs_pattern p1 p2 = match p1, p2 with
 | Const_cs gr1, Const_cs gr2 -> eq_gr gr1 gr2
 | Prod_cs, Prod_cs -> true
@@ -241,8 +233,6 @@ let pr_cs_pattern = function
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
 
-let pr_pattern (p,c) = pr_cs_pattern p
-
 let open_canonical_structure i (_,o) =
   if Int.equal i 1 then
     let lo = compute_canonical_projections o in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fb426efed..c9d4e388d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -736,10 +736,6 @@ let fix_recarg ((recindices,bodynum),_) stack =
   with Not_found ->
     None
 
-type 'a reduced_state = 
-  | NotReducible
-  | Reduced of constr
-
 (** Generic reduction function with environment
 
     Here is where unfolded constant are stored in order to be
@@ -1082,13 +1078,6 @@ let whd_betadeltaiota_stack env =
 let whd_betadeltaiota env =
   red_of_state_red (whd_betadeltaiota_state env)
 
-let whd_betadeltaiota_state_using ts env =
-  raw_whd_state_gen (Closure.RedFlags.red_add_transparent betadeltaiota ts) env
-let whd_betadeltaiota_stack_using ts env =
-  stack_red_of_state_red (whd_betadeltaiota_state_using ts env)
-let whd_betadeltaiota_using ts env =
-  red_of_state_red (whd_betadeltaiota_state_using ts env)
-
 let whd_betadeltaiotaeta_state env = raw_whd_state_gen betadeltaiotaeta env
 let whd_betadeltaiotaeta_stack env =
   stack_red_of_state_red (whd_betadeltaiotaeta_state env)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 53c2603d8..aa33c3286 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -16,7 +16,6 @@ open Inductiveops
 open Names
 open Reductionops
 open Environ
-open Declarations
 open Termops
 
 type retype_error =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b405afa93..a32d54b5e 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -59,11 +59,6 @@ let value_of_evaluable_ref env evref u =
       raise (Invalid_argument "value_of_evaluable_ref"))
   | EvalVarRef id -> Option.get (pi2 (lookup_named id env))
 
-let constr_of_evaluable_ref evref u =
-  match evref with
-  | EvalConstRef con -> mkConstU (con,u)
-  | EvalVarRef id -> mkVar id
-
 let evaluable_of_global_reference env = function
   | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
   | VarRef id when is_evaluable_var env id -> EvalVarRef id
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 363292ec0..d9cd58cea 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -494,13 +494,6 @@ let occur_meta_or_existential c =
     | _ -> iter_constr occrec c
   in try occrec c; false with Occur -> true
 
-let occur_const s c =
-  let rec occur_rec c = match kind_of_term c with
-    | Const (sp,_) when sp=s -> raise Occur
-    | _ -> iter_constr occur_rec c
-  in
-  try occur_rec c; false with Occur -> true
-
 let occur_evar n c =
   let rec occur_rec c = match kind_of_term c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 6fa5b8896..d89731147 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -375,11 +375,6 @@ let pr_priority = function
 | None -> mt ()
 | Some i -> spc () ++ str "|" ++ spc () ++ int i
 
-let pr_poly p = 
-  if Flags.is_universe_polymorphism () then
-    if not p then str"Monomorphic " else mt ()
-  else if p then str"Polymorphic " else mt ()
-
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
diff --git a/printing/printer.ml b/printing/printer.ml
index cb10f9661..3b5c80c62 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -727,8 +727,6 @@ let pr_assumptionset env s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-open Typeclasses
-
 let xor a b = 
   (a && not b) || (not a && b)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 695e8ab6e..d58d1f5a0 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -7,9 +7,7 @@
 (************************************************************************)
 
 open Util
-open Names
 open Namegen
-open Term
 open Termops
 open Environ
 open Reductionops
diff --git a/stm/stm.ml b/stm/stm.ml
index 5733b0c32..85c3838dc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -214,7 +214,6 @@ module VCS : sig
   val goals : id -> int -> unit
   val set_state : id -> state -> unit
   val get_state : id -> state option
-  val forget_state : id -> unit
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : start:id -> stop:id -> vcs
@@ -366,7 +365,6 @@ end = struct
     | None -> raise Vcs_aux.Expired
   let set_state id s = (get_info id).state <- Some s
   let get_state id = (get_info id).state
-  let forget_state id = (get_info id).state <- None
   let reached id b =
     let info = get_info id in
     if b then info.n_reached <- info.n_reached + 1
@@ -690,19 +688,9 @@ end = struct
         Stateid.t * Stateid.t * std_ppcmds *
           (Stateid.t * State.frozen_state) list
     | RespFeedback of Interface.feedback
-    | RespGetCounterFreshLocalUniv
     | RespGetCounterNewUnivLevel
-  let pr_response = function
-    | RespBuiltProof _ -> "Sucess"
-    | RespError _ -> "Error"
-    | RespFeedback { Interface.id = Interface.State id } ->
-        "Feedback on " ^ Stateid.to_string id
-    | RespFeedback _ -> assert false
-    | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv"
-    | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel"
 
   type more_data =
-    | MoreDataLocalUniv of Univ.universe list
     | MoreDataUnivLevel of Univ.universe_level list
  
   type task =
@@ -987,7 +975,6 @@ end = struct
                    Pp.feedback (Interface.InProgress ~-1) *)
                 last_task := None;
                 raise KillRespawn
-            | _, RespGetCounterFreshLocalUniv -> assert false (* Deprecated function *)
                 (* marshal_more_data oc (MoreDataLocalUniv *)
                 (*   (CList.init 10 (fun _ -> Universes.fresh_local_univ ()))); *)
                 (* loop () *)
@@ -1090,7 +1077,7 @@ end = struct
     Universes.set_remote_new_univ_level (bufferize (fun () ->
       marshal_response !slave_oc RespGetCounterNewUnivLevel;
       match unmarshal_more_data !slave_ic with
-      | MoreDataUnivLevel l -> l | _ -> assert false));
+      | MoreDataUnivLevel l -> l));
     let working = ref false in
     slave_handshake ();
     while true do
diff --git a/tactics/auto.ml b/tactics/auto.ml
index aa70d55cc..4f5f53ef0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -141,12 +141,6 @@ type search_entry = stored_data list * stored_data list * Bounded_net.t
 
 let empty_se = ([],[],Bounded_net.create ())
 
-let eq_constr_or_reference x y = 
-  match x, y with
-  | IsConstr (x,_), IsConstr (y,_) -> eq_constr x y
-  | IsGlobRef x, IsGlobRef y -> eq_gr x y
-  | _, _ -> false
-
 let eq_pri_auto_tactic (_, x) (_, y) =
   if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
     match x.code,y.code with
@@ -189,11 +183,6 @@ let is_transparent_gr (ids, csts) = function
 
 let dummy_goal = Goal.V82.dummy_goal
 
-let instantiate_constr_or_ref env sigma c =
-  let c, ctx = Universes.fresh_global_or_constr_instance env c in
-  let cty = Retyping.get_type_of env sigma c in
-    (c, cty), ctx
-
 let strip_params env c = 
   match kind_of_term c with
   | App (f, args) -> 
@@ -875,10 +864,6 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make ()
 
 type hnf = bool
 
-let pr_hint_term = function
-  | IsConstr (c,_) -> pr_constr c
-  | IsGlobRef gr -> pr_global gr
-
 type hints_entry =
   | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index a95d71443..02dded782 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -9,11 +9,8 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Util
-open Names
 open Locus
-open Tacexpr
 open Misctypes
-open Tacinterp
 
 DECLARE PLUGIN "coretactics"
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index bb7d2f0d2..fd5310e04 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -211,7 +211,7 @@ module SearchProblem = struct
 
   let success s = List.is_empty (sig_it s.tacres)
 
-  let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
+(*   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *)
 
   let filter_tactics glls l =
 (*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 617475bb7..9b600409a 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -17,7 +17,6 @@ open Term
 open Indrec
 open Declarations
 open Typeops
-open Termops
 open Ind_tables
 
 (* Induction/recursion schemes *)
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 7909b669b..c18fd31d0 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -82,8 +82,6 @@ let solveNoteqBranch side =
 
 let make_eq () =
 (*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ())
-let make_eq_refl () =
-(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
 
 let mkDecideEqGoal eqonleft op rectype c1 c2 =
   let equality    = mkApp(make_eq(), [|rectype; c1; c2|]) in
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index dc41cf8e3..a2a8675a8 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -72,9 +72,6 @@ let glob_occs ist l = l
 
 let subst_occs evm l = l
 
-type occurrences_or_var = int list or_var
-type occurrences = int list
-
 ARGUMENT EXTEND occurrences
   PRINTED BY pr_int_list_full
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 130e66720..a8bcec288 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -387,12 +387,6 @@ let match_eq eqn eq_pat =
 let no_check () = true
 let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
 
-let build_coq_jmeq_data_in env =
-  build_coq_jmeq_data (), Univ.ContextSet.empty
-
-let build_coq_identity_data_in env =
-  build_coq_identity_data (), Univ.ContextSet.empty
-
 let equalities =
   [coq_eq_pattern, no_check, build_coq_eq_data;
    coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
@@ -442,11 +436,6 @@ let dest_nf_eq gls eqn =
 
 (*** Sigma-types *)
 
-(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
-let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
-let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
-
 let match_sigma ex =
   match kind_of_term ex with
   | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f -> 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 7309e2275..b4b8d468c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -36,12 +36,7 @@ open Goal
 open Environ
 open Tacinterp
 open Termops
-open Genarg
-open Extraargs
-open Pcoq.Constr
-open Entries
 open Libnames
-open Evarutil
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -76,7 +71,6 @@ let find_global dir s =
 
 (** Global constants. *)
 
-let gen_reference dir s = Coqlib.gen_reference "rewrite" dir s
 let coq_eq_ref = find_reference ["Init"; "Logic"] "eq"
 let coq_eq = find_global ["Init"; "Logic"] "eq"
 let coq_f_equal = find_global ["Init"; "Logic"] "f_equal"
@@ -118,13 +112,6 @@ let new_cstr_evar (evd,cstrs) env t =
 let e_new_cstr_evar evars env t =
   let evd', t = new_cstr_evar !evars env t in evars := evd'; t
 
-let new_goal_evar (evd,cstrs) env t =
-  let evd', t = Evarutil.new_evar evd env t in
-    (evd', cstrs), t
-
-let e_new_goal_evar evars env t =
-  let evd', t = new_goal_evar !evars env t in evars := evd'; t
-
 (** Building or looking up instances. *)
 
 let extends_undefined evars evars' =
@@ -161,7 +148,6 @@ module GlobalBindings (M : sig
   val relation : string list * string
   val app_poly : env -> evars -> (evars -> evars * constr) -> constr array -> evars * constr
   val arrow : evars -> evars * constr
-  val coq_inverse : evars -> evars * constr
 end) = struct
   open M
   let relation : evars -> evars * constr = find_global (fst relation) (snd relation)
@@ -608,14 +594,6 @@ let solve_remaining_by by env prf =
       indep env.evd
     in { env with evd = evd' }, prf
 
-let extend_evd sigma ext sigma' =
-  Evar.Set.fold (fun i acc ->
-    Evd.add acc i (Evarutil.nf_evar_info sigma' (Evd.find sigma' i)))
-    ext sigma
-
-let shrink_evd sigma ext =
-  Evar.Set.fold (fun i acc -> Evd.remove acc i) ext sigma
-
 let no_constraints cstrs = 
   fun ev _ -> not (Evar.Set.mem ev cstrs)
 
@@ -707,10 +685,6 @@ let make_eq () =
 let make_eq_refl () =
 (*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
 
-let get_rew_rel r = match r.rew_prf with
-  | RewPrf (rel, prf) -> rel
-  | RewCast c -> mkApp (make_eq (),[| r.rew_car; r.rew_from; r.rew_to |])
-
 let get_rew_prf r = match r.rew_prf with
   | RewPrf (rel, prf) -> rel, prf 
   | RewCast c ->
@@ -1289,25 +1263,6 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = t';
 			   rew_prf = RewCast ckind; rew_evars = evars })
 	
-    let fold c : strategy =
-      fun env avoid t ty cstr evars ->
-(* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
-	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
-	let unfolded =
-	  try Tacred.try_red_product env sigma c
-	  with e when Errors.noncritical e ->
-            error "fold: the term is not unfoldable !"
-	in
-	  try
-	  let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ())
-	    unfolded t in
-	    let c' = Evarutil.nf_evar sigma c in
-	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
-			   rew_prf = RewCast DEFAULTcast; 
-			   rew_evars = (sigma, snd evars) })
-	  with e when Errors.noncritical e -> None
-
-
     let fold_glob c : strategy =
       fun env avoid t ty cstr evars ->
 (* 	let sigma, (c,_) = Tacinterp.interp_open_constr_with_bindings is env (goalevars evars) c in *)
@@ -1426,9 +1381,6 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
     | Some None -> Some None
     | None -> None
 		   
-let rewrite_refine (evd,c) = 
-  Tacmach.refine c
-
 let cl_rewrite_clause_tac ?abs strat meta clause gl =
   let evartac evd = Refiner.tclEVARS (Evd.clear_metas evd) in
   let treat res =
@@ -1582,30 +1534,11 @@ let cl_rewrite_clause_strat strat clause =
 let cl_rewrite_clause l left2right occs clause gl =
   cl_rewrite_clause_strat (rewrite_with (general_rewrite_unif_flags ()) l left2right occs) clause gl
 
-let occurrences_of = function
-  | n::_ as nl when n < 0 -> (false,List.map abs nl)
-  | nl ->
-      if List.exists (fun n -> n < 0) nl then
-	error "Illegal negative occurrence number.";
-      (true,nl)
-
-open Extraargs
-
-let apply_constr_expr c l2r occs = fun env avoid t ty cstr evars ->
-  let evd, c = Constrintern.interp_open_constr (goalevars evars) env c in
-    apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) 
-      l2r None occs env avoid t ty cstr (evd, cstrevars evars)
-
 let apply_glob_constr c l2r occs = fun env avoid t ty cstr evars ->
   let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in
     apply_lemma (general_rewrite_unif_flags ()) (Evd.empty, (c, NoBindings)) 
       l2r None occs env avoid t ty cstr (evd, cstrevars evars)
 
-let interp_constr_list env sigma =
-  List.map (fun c -> 
-	      let evd, c = Constrintern.interp_open_constr sigma env c in
-		(evd, (c, NoBindings)), true, None)
-
 let interp_glob_constr_list env sigma =
   List.map (fun c -> 
 	      let evd, c = Pretyping.understand_tcc sigma env c in
@@ -2112,74 +2045,6 @@ let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
 let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
 let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
 
-let implify id gl =
-  let (_, b, ctype) = pf_get_hyp gl id in
-  let binders,concl = decompose_prod_assum ctype in
-  let evm, ctype' =
-    match binders with
-    | (_, None, ty as hd) :: tl when noccurn 1 concl ->
-	let env = Environ.push_rel_context tl (pf_env gl) in
-	let sigma = project gl in
-	let tyhd = Retyping.get_type_of env sigma ty
-	and tyconcl = Retyping.get_type_of (Environ.push_rel hd env) sigma concl in
-	let ((sigma,_), app), unfold = 
-	  PropGlobal.arrow_morphism env (sigma, Evar.Set.empty) tyhd 
-	    (subst1 mkProp tyconcl) ty (subst1 mkProp concl) 
-	in
-	  sigma, it_mkProd_or_LetIn app tl
-    | _ -> project gl, ctype
-  in tclTHEN (Refiner.tclEVARS evm) (Tacmach.convert_hyp (id, b, ctype')) gl
-
-let rec fold_matches env sigma c =
-  map_constr_with_full_binders Environ.push_rel 
-    (fun env c ->
-      match kind_of_term c with
-      | Case _ ->
-          let cst, env, c', _eff = fold_match ~force:true env sigma c in
-	    fold_matches env sigma c'
-      | _ -> fold_matches env sigma c)
-    env c
-
-let fold_match_tac c gl =
-  let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
-  let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
-    change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
-
-let fold_matches_tac c gl =
-  let c' = fold_matches (pf_env gl) (project gl) c in
-  (* let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in *)
-    change (Some (snd (Patternops.pattern_of_constr (project gl) c))) c' onConcl gl
-
-let myapply id l gl =
-  let gr = id in
-  let _, impls = List.hd (Impargs.implicits_of_global gr) in
-  let env = pf_env gl in
-  let evars = ref (project gl) in
-  let evd, ty = fresh_global env !evars gr in
-  let _ = evars := evd in
-  let app =
-    let rec aux ty impls args args' =
-      match impls, kind_of_term ty with
-      | Some (_, _, (_, _)) :: impls, Prod (n, t, t') ->
-	let arg = Evarutil.e_new_evar evars env t in
-	  aux (subst1 arg t') impls args (arg :: args')
-      | None :: impls, Prod (n, t, t') ->
-	(match args with
-	| [] ->
-	  if dependent (mkRel 1) t' then
-	    let arg = Evarutil.e_new_evar evars env t in
-	      aux (subst1 arg t') impls args (arg :: args')
-	  else
-	    let arg = Evarutil.mk_new_meta () in
-	      evars := meta_declare (destMeta arg) t !evars;
-	      aux (subst1 arg t') impls args (arg :: args')
-	| arg :: args -> 
-	  aux (subst1 arg t') impls args (arg :: args'))
-      | _, _ -> mkApp (Universes.constr_of_global gr, Array.of_list (List.rev args'))
-    in aux ty impls l []
-  in
-    tclTHEN (Refiner.tclEVARS !evars) (apply app) gl
-
 let get_lemma_proof f env evm x y = 
   let (evm, _), c = f env (evm,Evar.Set.empty) x y in
     evm, c
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 35952c9dd..f68f75359 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -43,10 +43,6 @@ let error_syntactic_metavariables_not_allowed loc =
 let error_tactic_expected loc =
   user_err_loc (loc,"",str "Tactic expected.")
 
-let skip_metaid = function
-  | AI x -> x
-  | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
-
 (** Generic arguments *)
 
 type glob_sign = Genintern.glob_sign = {
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b7018fe45..1d76f4afd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -294,9 +294,6 @@ let interp_ident = interp_ident_gen false
 let interp_fresh_ident = interp_ident_gen true
 let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl)
 
-let interp_global ist gl gr = 
-  Evd.fresh_global (pf_env gl) (project gl) gr
-
 (* Interprets an optional identifier which must be fresh *)
 let interp_fresh_name ist env = function
   | Anonymous -> Anonymous
@@ -578,14 +575,6 @@ let interp_auto_lemmas ist env sigma lems =
 let pf_interp_type ist gl =
   interp_type ist (pf_env gl) (project gl)
 
-let new_interp_type ist c k =
-  let open Proofview.Goal in
-  let open Proofview.Notations in
-  Proofview.Goal.raw_enter begin fun gl ->
-    let (sigma, c) = interp_type ist (env gl) (sigma gl) c in
-    Proofview.V82.tclEVARS sigma <*> k c
-  end
-
 (* Interprets a reduction expression *)
 let interp_unfold ist env (occs,qid) =
   (interp_occurrences ist occs,interp_evaluable ist env qid)
@@ -953,8 +942,6 @@ struct
     Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
     Proofview.tclUNIT (Depends (List.concat l))
 
-  let goal = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-
   let enter f =
     bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
       (fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index aa090b715..4dd4b0aa8 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -15,7 +15,6 @@ open Misctypes
 open Globnames
 open Term
 open Genredexpr
-open Inductiveops
 open Patternops
 open Pretyping
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cc1528797..48fd44b4a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -224,6 +224,8 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
+  val onHyps      : ([ `NF ] Proofview.Goal.t -> named_context) ->
+                    (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
   val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 2d9b4da96..bdacf85a8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -11,7 +11,6 @@
 open Term
 open Hipattern
 open Names
-open Globnames
 open Pp
 open Genarg
 open Stdarg
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e05f4bcfe..f8d7a197b 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -337,11 +337,11 @@ struct
     | _ -> assert false
 
   (* debug *)
-  let rec pr_term_pattern p =
+(*  let rec pr_term_pattern p =
     (fun pr_t -> function
        | Term t -> pr_t t
        | Meta m -> str"["++Pp.int (Obj.magic m)++str"]"
-    ) (pr_dconstr pr_term_pattern) p
+    ) (pr_dconstr pr_term_pattern) p*)
 
   let search_pat cpat dpat dn =
     let whole_c = cpat in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d28445f17..13696a17c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -228,9 +228,6 @@ let declare_assumption is_coe (local,p,kind) (c,ctx) imps impl nl (_,ident) = ma
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let declare_assumptions_hook = ref ignore
-let set_declare_assumptions_hook = (:=) declare_assumptions_hook
-
 let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
   let ty, impls = interp_type_evars_impls evdref env c in
@@ -585,9 +582,6 @@ type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
 
-type one_inductive_expr =
-  lident * local_binder list * constr_expr option * constructor_expr list
-
 let do_mutual_inductive indl poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
@@ -1079,11 +1073,6 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
-let collect_evars_of_term evd c ty =
-  let evars = Evar.Set.union (evars_of_term c) (evars_of_term ty) in
-    Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
-      evars Evd.empty
-      
 let do_program_recursive local p fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, evd), fix, info = 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 76d2b89c6..a011fc6a6 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -212,7 +212,7 @@ let display_cmd_header loc com =
   Pp.flush_all ()
 
 let rec vernac_com verbosely checknav (loc,com) =
-  let rec interp = function
+  let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
 	let st = save_translator_coqdoc () in