NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
NCic.Inductive (true,leftno,[itl],_) ->
List.map (fun s-> mk_elim status uri leftno itl (ast_of_sort s) (`Elim s))
(NCic.Prop::
let bvars =
HExtlib.mk_list underscore i @ [bvar,None] @
HExtlib.mk_list underscore (argsno - i -1) in
let bvars =
HExtlib.mk_list underscore i @ [bvar,None] @
HExtlib.mk_list underscore (argsno - i -1) in