Removing dead code.

Author: ppedrot

dev/top_printers.ml

@@ -22,7 +22,6 @@ open Evd
 open Goptions
 open Genarg
 open Clenv
-open Universes
 
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true

intf/tacexpr.mli

@@ -10,12 +10,10 @@ open Loc
 open Names
 open Constrexpr
 open Libnames
-open Globnames
 open Nametab
 open Genredexpr
 open Genarg
 open Pattern
-open Decl_kinds
 open Misctypes
 open Locus
 

kernel/cbytegen.mli

@@ -1,4 +1,3 @@
-open Names
 open Cbytecodes
 open Cemitcodes
 open Term

kernel/cemitcodes.ml

@@ -10,7 +10,6 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
-open Names
 open Term
 open Cbytecodes
 open Copcodes

kernel/closure.ml

@@ -771,24 +771,6 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-
-let rec get_parameters depth n argstk =
-  match argstk with
-      Zapp args::s ->
-        let q = Array.length args in
-        if n > q then Array.append args (get_parameters depth (n-q) s)
-        else if Int.equal n q then [||]
-        else Array.sub args 0 n
-    | Zshift(k)::s -> 
-      get_parameters (depth-k) n s
-    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-	if Int.equal n 0 then [||]
-	else raise Not_found (* Trying to eta-expand a partial application..., should do 
-				eta expansion first? *)
-    | _ -> assert false
-	(* strip_update_shift_app only produces Zapp and Zshift items *)
-
-
 (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments

kernel/declareops.mli

@@ -9,7 +9,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Context
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)

kernel/fast_typeops.mli

@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Univ
 open Term
-open Context
 open Environ
-open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     

kernel/indtypes.ml

@@ -654,7 +654,6 @@ let used_section_variables env inds =
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_appvect n m = rel_vect n (List.length m)
 
 exception UndefinableExpansion
 

kernel/inductive.ml

@@ -447,13 +447,6 @@ type subterm_spec =
 
 let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
-let pp_recarg = function
-  | Norec -> Pp.str "Norec"
-  | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
-  | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2

kernel/names.ml

@@ -571,7 +571,6 @@ let constr_modpath (ind,_) = ind_modpath ind
 
 let ith_mutual_inductive (mind, _) i = (mind, i)
 let ith_constructor_of_inductive ind i = (ind, i)
-let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u)
 let inductive_of_constructor (ind, i) = ind
 let index_of_constructor (ind, i) = i