Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
| CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in