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 =
List.flatten (
List.rev_map
(fun (_,ty) -> domain_rev_of_term [] ty) cl) @
- domain_rev_of_term [] ty) tyl)
+ domain_rev_of_term [] ty) tyl) in
+ let dom =
+ List.fold_left
+ (fun dom (_,ty) ->
+ domain_rev_of_term [] ty @ dom
+ ) dom params
in
List.filter
(fun name ->
let dom =
List.flatten
(List.rev_map (fun (_,ty) -> domain_rev_of_term [] ty) fields) in
- let dom' =
+ let dom =
List.filter
(fun name->
not ( List.exists (fun (name',_) -> name = Id name') params
|| List.exists (fun (name',_) -> name = Id name') fields)
) dom
in
- dom' @ domain_rev_of_term [] ty
+ List.fold_left
+ (fun dom (_,ty) ->
+ domain_rev_of_term [] ty @ dom
+ ) (dom @ domain_rev_of_term [] ty) params
in
rev_uniq domain_rev