+ | [ IDENT "inductive" | IDENT "Inductive" ]; fst_name = IDENT;
+ params = LIST0 [
+ PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
+ typ = term; PAREN ")" -> (names, typ) ];
+ SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
+ fst_constructors = LIST0 constructor SEP SYMBOL "|" ->
+ let params =
+ List.fold_right
+ (fun (names, typ) acc ->
+ (List.map (fun name -> (name, typ)) names) @ acc)
+ params []
+ in
+ let fst_ind_type = (fst_name, true, fst_typ, fst_constructors) in
+ let ind_types = [fst_ind_type] in
+ return_command loc (TacticAst.Inductive (params, ind_types))