Removing dead code.

12 files changed, 2 insertions, 137 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1c9796b4de..d93574b47d 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 7222085e18..66d65bab6a 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 0a9b376980..a842134df5 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 e36e16c05b..53d1a8a0e6 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 43552ef542..21395af027 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 6c490d7b9a..8b9e6e633a 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 5ae49e5637..91b851d12f 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 7250217d68..35ac90de57 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 fb426efede..c9d4e388d6 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 53c2603d8c..aa33c32863 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 b405afa93c..a32d54b5e6 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 363292ec04..d9cd58cea8 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