- NCic.Inductive(ind, leftno + List.length vars, itl, (`Provided, `Regular)),
+ NCic.Inductive(ind, leftno + List.length
+ (List.filter (fun v ->
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph v) with
+ Cic.Variable (_,Some _,_,_,_) -> false
+ | Cic.Variable (_,None,_,_,_) -> true
+ | _ -> assert false)
+ vars)
+ , itl, (`Provided, `Regular)),