3 files changed, 1 insertions, 81 deletions
diff --git a/library/impargs.ml b/library/impargs.ml
index b334092b92..5b52f19760 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -68,7 +68,7 @@ let declare_inductive_implicits sp =
   let mib = Global.lookup_mind sp in
   let imps_one_inductive mip =
     (auto_implicits (body_of_type mip.mind_arity),
-     Array.map auto_implicits mip.mind_lc)
+     Array.map (fun c -> auto_implicits (body_of_type c)) mip.mind_lc)
   in
   let imps = Array.map imps_one_inductive mib.mind_packets in
   inductives_table := Spmap.add sp imps !inductives_table
diff --git a/library/indrec.ml b/library/indrec.ml
index f83138b3d0..da5aeec345 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -398,66 +398,3 @@ let type_rec_branches recursive env sigma ind pt p c =
   else 
     type_case_branches env sigma ind pt p c
 
-(***************************************************)
-(* Building ML like case expressions without types *)
-
-let concl_n env sigma = 
-  let rec decrec m c = if m = 0 then c else 
-    match whd_betadeltaiota env sigma c with
-      | DOP2(Prod,_,DLAM(n,c_0)) -> decrec (m-1) c_0
-      | _                        -> failwith "Typing.concl_n"
-  in 
-  decrec
-
-let count_rec_arg j = 
-  let rec crec i = function 
-    | [] -> i 
-    | (Mrec k::l) -> crec (if k=j then (i+1) else i) l
-    | (_::l) -> crec i l
-  in 
-  crec 0
-
-(* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
- * K parameters. Then then build_notdep builds the predicate
- * [a_bar:A'_bar](lift k pred) 
- * where A'_bar = A_bar[p_bar <- globargs] *)
-
-let build_notdep_pred env sigma indf pred =
-  let arsign,_ = get_arity env sigma indf in
-  let nar = List.length arsign in
-  it_lambda_name env (lift nar pred) arsign
-
-
-let pred_case_ml_fail env sigma isrec (IndType (indf,realargs)) (i,ft) =
-  let pred =
-    let mispec,_ = dest_ind_family indf in
-    let recargs = mis_recarg mispec in
-    assert (Array.length recargs <> 0);
-    let recargi = recargs.(i-1) in
-    let j = mis_index mispec in
-    let nbrec = if isrec then count_rec_arg j recargi else 0 in
-    let nb_arg = List.length (recargs.(i-1)) + nbrec in
-    let pred = concl_n env sigma nb_arg ft in
-    if noccur_between 1 nb_arg pred then 
-      lift (-nb_arg) pred
-    else 
-      failwith "Dependent"
-  in
-  if realargs = [] then 
-    pred
-  else (* we try with [_:T1]..[_:Tn](lift n pred) *)
-    build_notdep_pred env sigma indf pred  
-
-let pred_case_ml env sigma isrec indt lf (i,ft) = 
-    pred_case_ml_fail env sigma isrec indt (i,ft)
-
-(* similar to pred_case_ml but does not expect the list lf of braches *)
-let pred_case_ml_onebranch env sigma isrec indt (i,f,ft) = 
-    pred_case_ml_fail env sigma isrec indt (i,ft)
-
-(* Used in Program only *)      
-let make_case_ml isrec pred c ci lf = 
-  if isrec then 
-    DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
-  else 
-    mkMutCaseA ci pred c lf
diff --git a/library/indrec.mli b/library/indrec.mli
index bfb22f4c99..728b3c5dc2 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -37,20 +37,3 @@ val make_rec_branch_arg :
   env -> 'a evar_map ->
     int * ('b * constr) option array * int ->
     constr -> constructor_summary -> recarg list -> constr
-
-val pred_case_ml_onebranch : env -> 'c evar_map -> bool ->
-  inductive_type -> int * constr * constr -> constr 
-
-(*i Info pour JCF : déplacé dans pretyping, sert à Program
-val transform_rec : env -> 'c evar_map -> (constr array) 
-  -> (constr * constr) -> constr
-i*)
-
-(*i Utilisés dans Program
-val pred_case_ml : env -> 'c evar_map -> bool ->
-  constr * (inductive * constr list * constr list)
-  ->  constr array -> int * constr  ->constr
-val make_case_ml :
-  bool -> constr -> constr -> case_info -> constr array -> constr
-i*)
-