let field_names = List.map fst fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | TacticAst.Theorem (_,name,ty,bo) ->
+ | TacticAst.Theorem (flavour, name, ty, bo) ->
+ let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
- match bo with
+ (match bo with
None ->
- Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],[])
+ Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
| Some bo ->
let bo' = Some (interpretate_term [] env None false bo) in
- Cic.Constant (name,bo',ty',[],[])
+ Cic.Constant (name,bo',ty',[],attrs))
+
(* e.g. [5;1;1;1;2;3;4;1;2] -> [2;1;4;3;5] *)
let rev_uniq =