NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
- List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+ List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes status))
| _ -> []
;;