+let mk_record types lpsno fields =
+ match mk_pre_inductive types lpsno with
+ | lpars, [name, _, ty, [_, cty]] ->
+ let map (fields, cty) (name, coercion, arity) =
+ match cty with
+ | C.AProd (_, _, w, t) ->
+ (name, w, coercion, arity) :: fields, t
+ | _ ->
+ assert false
+ in
+ let rev_fields, _ = List.fold_left map ([], cty) fields in
+ let fields = List.rev rev_fields in
+ let obj = N.Record (lpars, name, ty, fields) in
+ G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
+ | _ -> assert false
+